valuationSubring_isPrincipalIdealRing

English

For a valuation v with cyclic, nontrivial value group, the valuation subring associated to v is a principal ideal ring.

Русский

Для оценки v с циклической ненулевой группой значений связанная с ней оценочная подкольцо является кольцом главных идеалов.

LaTeX

$$$ IsPrincipalIdealRing\\ (Subtype\\ x\\mapsto x\\in v.valuationSubring). $$$

Lean4

theorem valuationSubring_isPrincipalIdealRing [IsCyclic (valueGroup v)] [Nontrivial (valueGroup v)] :
    IsPrincipalIdealRing K₀ :=
  ⟨fun I ↦ ideal_isPrincipal v I⟩

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