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

Minor changes

Browse source
This commit is contained in:
Sayantan Santra 2023-06-15 19:34:20 -07:00
parent 01bce563a5
commit e9fbb1a521
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
CommAlg/krull.lean
View file

@ -86,7 +86,7 @@ lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
fun _ ↦ (WithBot.coe_le rfl).mpr (H1 _)
rw [←iSup_le_iff] at H1
have : ((n : ℕ∞) : WithBot ℕ∞) ≤ (((n - 1 : ℕ) : ℕ∞) : WithBot ℕ∞) := le_trans H H1
norm_cast at this
norm_cast at this
have that : n - 1 < n := by refine Nat.sub_lt h (by norm_num)
apply lt_irrefl (n-1) (trans that this)
· rintro ⟨I, h⟩
@ -278,7 +278,7 @@ lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim
have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this
unfold height
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 (ENat.one_le_iff_pos.mp this)
have nonpos_height : height P' ≤ 0 := by
have := height_le_krullDim P'
rw [h] at this