eq_X_pow_mul_shift_add_trunc — Mathlib

English

The same decomposition as above with the shift form, i.e. f = X^n · (mk i ↦ coeff(i+n) f) + (f.trunc n).

Русский

Та же декомпозиция, но в виде сдвига: f = X^n · (mk i ↦ coeff(i+n) f) + (f.trunc n).

LaTeX

$$$f = X^n \\cdot (\\text{mk } (\\lambda i, \\operatorname{coeff}(i+n) f)) + (f.trunc n)$$$

Lean4

/-- Split off the first `n` coefficients. -/
theorem eq_X_pow_mul_shift_add_trunc (n : ℕ) (f : R⟦X⟧) :
    f = X ^ n * (mk fun i ↦ coeff (i + n) f) + (f.trunc n : R⟦X⟧) := by
  rw [← (commute_X_pow _ n).eq, ← eq_shift_mul_X_pow_add_trunc]

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