English
Let H be a Weierstrass divisor at I for g. The sequence q_k in A[[X]] is defined inductively by q_0 = 0 and q_{k+1} = q_k + s_1 · u^{-1}, where s_1 is the power series with coefficients coeff(i+n)(f − g q_k) and u is the unit from the shifted coefficient, with n as above.
Русский
Пусть H — делитель Вейершстра по I для g. Последовательность q_k в A[[X]] задаётся индуктивно: q_0 = 0 и q_{k+1} = q_k + s_1 · u^{-1}, где s_1 — ряд с коэффициентами coeff(i+n)(f − g q_k), а u — единица, полученная из сдвинутого коэффициента; n — как выше.
LaTeX
$$$ q_0 = 0, \\\\quad q_{k+1} = q_k + s_1 \\cdot u^{-1}, \\\\quad s_1 = \\text{PowerSeries.mk}(i \\mapsto \\operatorname{coeff}_{i+n}(f - g q_k)), \\\\quad u = H.isUnit_shift.unit, \\\\quad n = (g.map (Ideal.Quotient.mk I)).order.toNat. $$$
Lean4
/-- The inductively constructed sequence `qₖ` in the proof of Weierstrass division. -/
noncomputable def seq (H : g.IsWeierstrassDivisorAt I) (f : A⟦X⟧) : ℕ → A⟦X⟧
| 0 => 0
| k + 1 =>
H.seq f k +
(mk fun i ↦ coeff (i + (g.map (Ideal.Quotient.mk I)).order.toNat) (f - g * H.seq f k)) * H.isUnit_shift.unit⁻¹
