coeff_f_sub_r_mem — Mathlib

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

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