coeff_div_sub_seq_mem — Mathlib

English

For all k,i, the i-th coefficient of H.seq f (k+1) − H.seq f k lies in I^k.

Русский

Для всех k,i i-й коэффициент разности H.seq f(k+1) − H.seq f k принадлежит I^k.

LaTeX

$$$ \\forall k,i:\\; \\operatorname{coeff}_i\\bigl(H.seq f (k+1) - H.seq f k\\bigr) \\in I^k. $$$

Lean4

theorem coeff_div_sub_seq_mem [IsPrecomplete I A] (k i : ℕ) : coeff i (H.div f - (H.seq f k)) ∈ I ^ k := by
  simpa [coeff_div, SModEq.sub_mem] using ((H.divCoeff f i).2 k).symm

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