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

new: Added minimalPrimes.toPrimeSpectrum

Browse source
This commit is contained in:
Sayantan Santra 2023-06-18 23:29:12 -05:00
parent 4f2005ca08
commit 9331874498
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
CommAlg/krull.lean
View file

@ -190,6 +190,14 @@ lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
rw [WithBot.coe_lt_coe] rw [WithBot.coe_lt_coe]
exact lt_height_iff' exact lt_height_iff'
/-- Convert elements in Ideal.minimalPrimes to PrimeSpectrum -/
lemma minimalPrimes.toPrimeSpectrum {R : Type _} [CommRing R] {I P : Ideal R} : P ∈ Ideal.minimalPrimes I → PrimeSpectrum R := by
unfold Ideal.minimalPrimes
intro Pmin
obtain ⟨L, _⟩ := Pmin
simp only [Set.mem_setOf_eq] at L
exact PrimeSpectrum.mk P L.1
#check height_le_krullDim #check height_le_krullDim
--some propositions that would be nice to be able to eventually --some propositions that would be nice to be able to eventually