eq_weierstrassDistinguished_mul_weierstrassUnit

English

The product of the distinguished parts of two power series equals the distinguished part of the product.

Русский

Произведение отличительных частей двух степенных рядов эквивалентно отличительной части их произведения.

LaTeX

$$$(g g')^{\text{dist}} = g^{\text{dist}} \cdot (g')^{\text{dist}}$$$

Lean4

theorem eq_weierstrassDistinguished_mul_weierstrassUnit (hg : g.map (IsLocalRing.residue A) ≠ 0) :
    g = g.weierstrassDistinguished hg * g.weierstrassUnit hg :=
  (g.exists_isWeierstrassFactorization hg).choose_spec.choose_spec.eq_mul

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