krullDimLE_one_iff_of_noZeroDivisors

English

For rings with no zero divisors, Ring.KrullDimLE 1 R is equivalent to every nonzero prime ideal being maximal.

Русский

Для колец без нулевых делителей KrullDimLE 1 R эквивалентно тому, что каждый ненулевой простой идеал является максимальным.

LaTeX

$$$[\text{NoZeroDivisors }R] \Rightarrow \mathrm{Ring.KrullDimLE }1\;R \iff \forall I:\mathrm{Ideal}(R), I \neq \perp \rightarrow I.IsPrime \rightarrow I.IsMaximal$$$

Lean4

theorem krullDimLE_one_iff_of_noZeroDivisors [NoZeroDivisors R] :
    Ring.KrullDimLE 1 R ↔ ∀ I : Ideal R, I ≠ ⊥ → I.IsPrime → I.IsMaximal :=
  by
  cases subsingleton_or_nontrivial R
  · exact iff_of_true inferInstance fun I h ↦ (h <| Subsingleton.elim ..).elim
  have := Ideal.bot_prime (α := R)
  exact Ring.krullDimLE_one_iff_of_isPrime_bot

Похожие утверждения