hasUnitMulPowIrreducibleFactorization

English

The ring k⟦X⟧ has a uniformizing parameter X: X is irreducible, and every nonzero f factors as a unit times a power of X.

Русский

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

LaTeX

$$$ X \text{ is irreducible and } \forall f \neq 0, \exists u \in k^{\times}, n \in \mathbb{N}, f = u \cdot X^{n}. $$$

Lean4

theorem hasUnitMulPowIrreducibleFactorization : HasUnitMulPowIrreducibleFactorization k⟦X⟧ :=
  ⟨X,
    And.intro X_irreducible
      (by
        intro f hf
        use f.order.toNat
        use Unit_of_divided_by_X_pow_order f
        simp only [Unit_of_divided_by_X_pow_order_nonzero hf]
        exact X_pow_order_mul_divXPowOrder)⟩

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