height_of_subsingleton — Mathlib

English

In a ring with a single element (subsingleton), every ideal has infinite height.

Русский

В кольце с единственным элементом (односвязном) высота каждого идеала равна бесконечности.

LaTeX

$$$[\text{Subsingleton}(R)]\;\Rightarrow\; I.\operatorname{height} = \top.$$$

Lean4

/-- In a trivial commutative ring, the height of any ideal is `∞`. -/
@[simp, nontriviality]
theorem height_of_subsingleton [Subsingleton R] : I.height = ⊤ := by rw [Subsingleton.elim I ⊤, Ideal.height_top]

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