maximalIdeal_eq — Mathlib

English

If an irreducible ϖ generates the maximal ideal, then ϖ is a uniformizer.

Русский

Если ирредуцируемый элемент порождает максимальный идеал, то он является uniformizer.

LaTeX

$$$\forall (R) [\mathrm{CommRing R}] [IsDomain R] [IsDiscreteValuationRing R] (\varpi : R)\; \mathrm{Irreducible } \varpi → IsLocalRing.maximalIdeal R = (\varpi)$$$

Lean4

theorem _root_.Irreducible.maximalIdeal_eq {ϖ : R} (h : Irreducible ϖ) : maximalIdeal R = Ideal.span { ϖ } :=
  (irreducible_iff_uniformizer _).mp h

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