ringKrullDimZero_iff_ringKrullDim_eq_zero

English

For a ring with KrullDimLE 0 and a Nontrivial ring, ringKrullDim R = 0 if and only if the local condition holds.

Русский

Для кольца с KrullDimLE 0 и ненулевого кольца: ringKrullDim R = 0 тогда и только тогда, когда выполняется локальная условие.

LaTeX

$$$\\text{ringKrullDim}(R) = 0 \\iff \\text{Ring.KrullDimLE }0~R$$$

Lean4

theorem ringKrullDimZero_iff_ringKrullDim_eq_zero [Nontrivial R] : Ring.KrullDimLE 0 R ↔ ringKrullDim R = 0 :=
  by
  rw [Ring.KrullDimLE, Order.krullDimLE_iff, le_antisymm_iff, ← ringKrullDim, Nat.cast_zero, iff_self_and]
  exact fun _ ↦ ringKrullDim_nonneg_of_nontrivial

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