is_generator — Mathlib

English

If π is a uniformizer, then the maximal ideal of the valuation subring is generated by π.

Русский

Если π — униформизатор, то максимальный идеал подкольца оценки порождается π.

LaTeX

$$$\operatorname{maximalIdeal}(v.valuationSubring) = \operatorname{span}\{ \pi \}.$$$

Lean4

theorem is_generator {π : v.valuationSubring} (hπ : IsUniformizer v π) :
    maximalIdeal v.valuationSubring = Ideal.span { π } :=
  Uniformizer.is_generator ⟨π, hπ⟩

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