krullDimLE_zero_iff — Mathlib

English

The statement Ring.KrullDimLE 0 R is equivalent to: every prime ideal is maximal.

Русский

Утверждение Ring.KrullDimLE 0 R эквивалентно тому, что каждый простый идеал максимален.

LaTeX

$$$Ring.KrullDimLE 0\\; R \\iff \\forall I: \\text{Ideal } R, I.IsPrime \\to I. IsMaximal$$$

Lean4

theorem krullDimLE_zero_iff : Ring.KrullDimLE 0 R ↔ ∀ I : Ideal R, I.IsPrime → I.IsMaximal :=
  by
  simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_zero, Order.krullDim_nonpos_iff_forall_isMax,
    (PrimeSpectrum.equivSubtype R).forall_congr_left, Subtype.forall, PrimeSpectrum.isMax_iff]
  rfl

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