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 #74 from ssavkar1/main

Browse source 
Implemented FieldisArtinian lemma
This commit is contained in:
ssavkar1 2023-06-15 10:28:00 -07:00 committed by GitHub
commit a75dadccd1
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 14 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
CommAlg/sameer(artinian-rings).lean
View file

@ -6,10 +6,20 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
import Mathlib.RingTheory.DedekindDomain.DVR import Mathlib.RingTheory.DedekindDomain.DVR
lemma FieldisArtinian (R : Type _) [CommRing R] (h: IsField R) : lemma FieldisArtinian (R : Type _) [CommRing R] (h : IsField R) :
IsArtinianRing R := by sorry IsArtinianRing R := by
let inst := h.toField
rw [isArtinianRing_iff, isArtinian_iff_wellFounded]
apply WellFounded.intro
intro I
constructor
intro J hJI
constructor
intro K hKJ
exfalso
rcases Ideal.eq_bot_or_top J with rfl | rfl
. exact not_lt_bot hKJ
. exact not_top_lt hJI
lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R] lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R]
(IsArt : IsArtinianRing R) : IsField (R) := by (IsArt : IsArtinianRing R) : IsField (R) := by