English
For each i, the i-th coefficient of H.div f equals the i-th component of H.divCoeff f, i.e., coeff_i(H.div f) = (H.divCoeff f i).1.
Русский
Каждый i-й коэффициент H.div f равен i-му компоненту H.divCoeff f, то есть \\mathrm{coeff}_i(H\\div f) = (H\\divCoeff f i)^{(1)}.
LaTeX
$$$ \\operatorname{coeff}_i\\bigl(H.\\text{div } f\\bigr) = (H.\\text{divCoeff } f i).1. $$$
Lean4
/-- The (bundled version of) coefficient of the limit `q` of the
inductively constructed sequence `qₖ` in the proof of Weierstrass division. -/
noncomputable def divCoeff [IsPrecomplete I A] (i : ℕ) :=
Classical.indefiniteDescription _ <|
IsPrecomplete.prec' (I := I) (fun k ↦ coeff i (H.seq f k)) fun {m} {n} hn ↦ by
induction n, hn using Nat.le_induction with
| base => rw [SModEq.def]
| succ n hn ih =>
refine ih.trans (SModEq.symm ?_)
rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top, ← map_sub]
exact Ideal.pow_le_pow_right hn (H.coeff_seq_succ_sub_seq_mem f n i)
