trunc_succ — Mathlib

English

For any f and n, trunc n.succ f equals trunc n f plus the nth monomial times the nth coefficient of f.

Русский

Для любого f и n: trunc n.succ f = trunc n f + Polynomial.monomial n (coeff n f).

LaTeX

$$$\\operatorname{trunc} (n+1) f = \\operatorname{trunc} n f + \\operatorname{Polynomial.monomial} n\\, (\\operatorname{coeff}_n f)$$$

Lean4

theorem trunc_succ (f : R⟦X⟧) (n : ℕ) : trunc n.succ f = trunc n f + Polynomial.monomial n (coeff n f) := by
  rw [trunc, Ico_zero_eq_range, sum_range_succ, trunc, Ico_zero_eq_range]

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