English
If f is Weierstrass division at g with r and I, then for suitable i, the coefficient of f − r lies in I.
Русский
Если f — дивизор Вайершстраса по g, q, r и I, то для подходящего i коэффициент f − r лежит в I.
LaTeX
$$$\\forall {A} [\\text{CommRing } A], \\; {f,g,q,r,I},\\; (H : f.IsWeierstrassDivisionAt g q r I) \\Rightarrow \\forall i,\\;\\text{...} \\Rightarrow \\operatorname{coeff} i (f - r) \\in I$$$
Lean4
theorem coeff_f_sub_r_mem (H : f.IsWeierstrassDivisionAt g q r I) {i : ℕ}
(hi : i < (g.map (Ideal.Quotient.mk I)).order.toNat) : coeff i (f - r : A⟦X⟧) ∈ I :=
by
replace H := H.2
rw [← sub_eq_iff_eq_add] at H
rw [H]
refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal i (fun j hj ↦ ?_) i le_rfl
have := coeff_of_lt_order_toNat _ (lt_of_le_of_lt hj hi)
rwa [coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at this