English
Let f,g be power series over a complete local ring A, with the image of g in the residue field nonzero. If n is the order of this image, then there exist a power series q and a polynomial r with deg r < n such that f = g q + r.
Русский
Пусть f,g — степенные серии над полным локальным кольцом A, образ g в остаточном полем не нуль. Пусть n — порядок этого образа; тогда существуют q ∈ A⟦X⟧ и r ∈ A[X], deg r < n, такие что f = g q + r.
LaTeX
$$$\exists q \in A\llbracket X\rrbracket, \exists r \in A[X], \deg r < n : f = g \cdot q + r$ где $n = \operatorname{ord}_{\bar A}(\bar g)$, \bar g = g \bmod \mathfrak m$.$$
Lean4
/-- **Weierstrass division** ([washington_cyclotomic], Proposition 7.2): let `f`, `g` be
power series over a complete local ring, such that
the image of `g` in the residue field is not zero. Let `n` be the order of the image of `g` in the
residue field. Then there exists a power series `q` and a polynomial `r` of degree `< n`, such that
`f = g * q + r`. -/
theorem exists_isWeierstrassDivision [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
(hg : g.map (IsLocalRing.residue A) ≠ 0) : ∃ q r, f.IsWeierstrassDivision g q r :=
⟨_, _, (IsWeierstrassDivisor.of_map_ne_zero hg).isWeierstrassDivisionAt_div_mod f⟩
-- Unfortunately there is no Unicode subscript `w`.
