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

Made very small changes

Browse source
This commit is contained in:
Sayantan Santra 2023-06-13 14:35:46 -07:00
parent 3730100c86
commit 7b8c0ba127
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
CommAlg/sayantan(dim_eq_zero_iff_field).lean
View file

@ -68,7 +68,7 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0)
have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this
rw [←Set.one_le_chainHeight_iff] at this rw [←Set.one_le_chainHeight_iff] at this
exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this) exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this)
have zero_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by have nonpos_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by
have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le
rw [iSup_le_iff] at this rw [iSup_le_iff] at this
exact Iff.mp WithBot.coe_le_zero (this P') exact Iff.mp WithBot.coe_le_zero (this P')