eq_mul_weierstrassDiv_add_weierstrassMod

English

If f,g satisfy Weierstrass division with quotient q and remainder r, then f = g q + r with r = f %ʷ g and q = f /ʷ g.

Русский

Если для степенной серии f и g выполняется деление Вайершстраса с частным q и остатком r, тогда f = g q + r и r = f %ʷ g, q = f /ʷ g.

LaTeX

$$$f = g\cdot( f /ʷ g) + (f %ʷ g)$$$

Lean4

theorem eq_mul_weierstrassDiv_add_weierstrassMod [IsAdicComplete (IsLocalRing.maximalIdeal A) A] :
    f = g * (f /ʷ g) + (f %ʷ g) :=
  by
  simp_rw [weierstrassDiv, weierstrassMod, dif_pos hg]
  exact ((IsWeierstrassDivisor.of_map_ne_zero hg).isWeierstrassDivisionAt_div_mod f).2

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