rescale_eq_subst — Mathlib

English

trunc is the map sending a power series to a polynomial by collecting finitely many terms up to n.

Русский

trunc переводит степенной ряд в многочлен, собирая конечное число членов до n.

LaTeX

$$$\operatorname{trunc} = \text{toFun} = \operatorname{truncFun}(n)$$$

Lean4

theorem rescale_eq_subst (a : σ → R) (f : MvPowerSeries σ R) : rescale a f = subst (a • X) f := by
  classical
  ext n
  rw [coeff_rescale]
  rw [coeff_subst (HasSubst.smul_X a), finsum_eq_sum _ (coeff_subst_finite (HasSubst.smul_X a) f n)]
  simp only [Pi.smul_apply', smul_eq_mul]
  rw [Finset.sum_eq_single n _ _]
  · simp [mul_comm, ← monomial_eq]
  · intro b hb hbn
    rw [← monomial_eq, coeff_monomial, if_neg (Ne.symm hbn), mul_zero]
  · intro hn
    simpa using hn

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