eq_shift_mul_X_pow_add_trunc — Mathlib

English

For every n and f, f equals X^n times the shifted coefficient series plus the truncation of f at n.

Русский

Для любого n и f выполняется разложение: f = X^n · (сдвинутая серия коэффициентов) + trunc n f.

LaTeX

$$$\\forall n, f:\\ R\\langle\\langle X \\rangle\\rangle, \\; f = X^n \\cdot \\bigl( \\text{mk } (\\lambda i, \\operatorname{coeff}(i+n) f) \\bigr) + (f.trunc n)$$$

Lean4

/-- Split off the first `n` coefficients. -/
theorem eq_shift_mul_X_pow_add_trunc (n : ℕ) (f : R⟦X⟧) :
    f = (mk fun i ↦ coeff (i + n) f) * X ^ n + (f.trunc n : R⟦X⟧) :=
  by
  ext j
  rw [map_add, Polynomial.coeff_coe, coeff_mul_X_pow', coeff_trunc]
  simp_rw [← not_le]
  split_ifs with h <;> simp [h]

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