height_bot — Mathlib

English

In a nontrivial ring, the height of the bottom ideal is zero.

Русский

В несобственном кольце высота нулевого идеала равна нулю.

LaTeX

$$$\operatorname{height}(\perp) = 0.$$$

Lean4

@[simp]
theorem height_bot [Nontrivial R] : (⊥ : Ideal R).height = 0 :=
  by
  obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes (R := R) (I := ⊥) top_ne_bot.symm
  simp only [Ideal.height, ENat.iInf_eq_zero]
  exact
    ⟨p, hp,
      haveI := hp.1.1;
      primeHeight_eq_zero_iff.mpr hp⟩

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