instUniqueFactorizationMonoid — Mathlib

English

The ring of formal power series k⟦X⟧ is a Unique Factorization Monoid: every nonzero element factors uniquely into irreducibles up to units.

Русский

Кольцо формальных степенных рядов k⟦X⟧ является уникальным факторизационным моноидом: каждый ненулевой элемент имеет уникальное разложение на ирредуцируемые элементы до единиц.

LaTeX

$$$ \text{UniqueFactorizationMonoid }(k[[X]]) . $$$

Lean4

instance : UniqueFactorizationMonoid k⟦X⟧ :=
  hasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid

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