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

change: Removed one unneeded line

Browse source
This commit is contained in:
Sayantan Santra 2023-06-17 20:04:04 -05:00
parent 9f0ed8cee3
commit 4f2005ca08
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
CommAlg/krull.lean
View file

@ -386,7 +386,6 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD
· unfold krullDim · unfold krullDim
apply @iSup_le (WithBot ℕ∞) _ _ _ _ apply @iSup_le (WithBot ℕ∞) _ _ _ _
intro I intro I
have PIR : IsPrincipalIdealRing (Polynomial K) := by infer_instance
by_cases I = ⊥ by_cases I = ⊥
· rw [← height_zero_iff_bot] at h · rw [← height_zero_iff_bot] at h
simp only [WithBot.coe_le_one, ge_iff_le] simp only [WithBot.coe_le_one, ge_iff_le]