SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 07:38:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

Merge pull request #18 from GTBarkley/Jayden

Browse source 
add lemma statement
This commit is contained in:
Jidong Wang 2023-06-11 21:42:33 -07:00 committed by GitHub
commit 45c58bf041
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
.DS_Store vendored Normal file
View file

Binary file not shown.

15
comm_alg/jayden(krull-dim-zero).lean Normal file
View file

@ -0,0 +1,15 @@
import Mathlib.RingTheory.Ideal.Basic
import Mathlib.RingTheory.Noetherian
import Mathlib.RingTheory.Artinian
import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
lemma dim_zero_Noetherian_is_Artinian (R : Type _) (IsNoetherianRing R) (krull_dim R = 0) : IsArtinianRing R := by sorry
-- Use Stacks project proof since it's broken into lemmas