English
Alternative construction: if every prime ideal is either minimal or maximal, then Ring.KrullDimLE 1 R holds.
Русский
Альтернативное построение: если каждый простой идеал либо минимален, либо максимален, тогда выполняется Ring.KrullDimLE 1 R.
LaTeX
$$$(\forall I:\mathrm{Ideal}(R), I.IsPrime \rightarrow I \in \mathrm{minimalPrimes}(R) \lor I.IsMaximal) \Rightarrow \mathrm{Ring.KrullDimLE }1\;R$$$
Lean4
/-- Alternative constructor for `Ring.KrullDimLE 1`, convenient for domains. -/
theorem mk₁' (H : ∀ I : Ideal R, I ≠ ⊥ → I.IsPrime → I.IsMaximal) : Ring.KrullDimLE 1 R :=
by
by_cases hR : (⊥ : Ideal R).IsPrime
· rwa [Ring.krullDimLE_one_iff_of_isPrime_bot]
suffices Ring.KrullDimLE 0 R from inferInstance
exact .mk₀ fun I hI ↦ H I (fun e ↦ hR (e ▸ hI)) hI
