English
For every k ≥ 0 and every i, if i ≥ n (the order from the Weierstrass divisor), then the i-th coefficient of f − g q_k lies in the ideal I^k, where q_k = H.seq f k and n is the order of g modulo I.
Русский
Для каждого k ≥ 0 и любого i, если i ≥ n (порядок делителя Вейершстра), то i-й коэффициент выражения f − g q_k лежит в идеале I^k, где q_k = H.seq f k и n — порядок g по отношению к I.
LaTeX
$$$ \\forall k \\in \\mathbb{N}, \\forall i \\in \\mathbb{N},\\; i \\ge n:\\; \\operatorname{coeff}_i\\bigl(f - g \\cdot q_k\\bigr) \\in I^k, \\text{ где } q_k = H.seq f k,\\; n = (g.map (Ideal.Quotient.mk I)).order.toNat. $$$
Lean4
theorem coeff_seq_mem (k : ℕ) {i : ℕ} (hi : i ≥ (g.map (Ideal.Quotient.mk I)).order.toNat) :
coeff i (f - g * H.seq f k) ∈ I ^ k := by
induction k generalizing hi i with
| zero => simp
| succ k hq =>
rw [seq]
set q := H.seq f k
set s := f - g * q
set n := (g.map (Ideal.Quotient.mk I)).order.toNat
have hs := s.eq_X_pow_mul_shift_add_trunc n
set s₀ := s.trunc n
set s₁ := PowerSeries.mk fun i ↦ coeff (i + n) s
set q' := q + s₁ * H.isUnit_shift.unit⁻¹
have key : f - g * q' = (s₀ : A⟦X⟧) - (g.trunc n : A⟦X⟧) * s₁ * H.isUnit_shift.unit⁻¹ :=
by
trans s + g * (q - q')
· simp_rw [s]; ring
simp_rw [q']
rw [sub_add_cancel_left, mul_neg, ← mul_assoc, mul_right_comm]
nth_rw 1 [g.eq_X_pow_mul_shift_add_trunc n]
rw [add_mul, mul_assoc, IsUnit.mul_val_inv, hs]
ring
rw [key, map_sub, Polynomial.coeff_coe, coeff_trunc, if_neg hi.not_gt, zero_sub, neg_mem_iff, pow_succ']
refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) i
refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (by simp [n, g.coeff_trunc_order_mem]) (fun i ↦ ?_) i
rw [coeff_mk]
exact hq (by simp)
