SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-10-16 19:43:55 -05:00
Code Issues Projects Releases Packages Wiki Activity

changed type of 1 in dim_le_one_of_dimLEOne

Browse source
This commit is contained in:
GTBarkley 2023-06-14 17:43:16 +00:00
parent 50ec280145
commit 7173aefe8d
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
CommAlg/krull.lean
View file

@ -197,7 +197,8 @@ height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain'
/-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib
applies only to dimension zero rings and domains of dimension 1. -/
lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ (1 : ℕ) := by
lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by
show _ → ((_ : WithBot ℕ∞) ≤ (1 : ℕ))
rw [krullDim_le_iff R 1]
intro H p
apply le_of_not_gt