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

Merge pull request #26 from ssavkar1/main

Browse source 
Defined 2 new lemmas
This commit is contained in:
ssavkar1 2023-06-12 13:36:51 -07:00 committed by GitHub
commit 5e45c14adc
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 17 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
.gitignore vendored
View file

@ -1,3 +1,4 @@
/build /build
/lake-packages/* /lake-packages/*
.DS_Store .DS_Store
.cache/

15
comm_alg/sameer(artinian-rings).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 quotientRing_is_Artinian (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R):
IsArtinianRing (R⧸I) := by sorry
#check Ideal.IsPrime
lemma IsPrimeMaximal (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R) (isPrime : Ideal.IsPrime I) : Ideal.IsMaximal I := by sorry
-- Use Stacks project proof since it's broken into lemmas