English
The coefficient of the product of two truncated power series equals the product of their truncations at index m, provided m ≤ n.
Русский
Коэффициент произведения двух усечённых степенных рядов равен коэффициенту произведения их усечений в позиции m при условии m ≤ n.
LaTeX
$$$$ \\operatorname{coeff}_{m}(\\,f \\cdot g\\,) = (\\operatorname{trunc}' R n f * \\operatorname{trunc}' R n g).coeff_{m} \\quad \\text{for } m \\le n. $$$$
Lean4
/-- The `n`th truncation of a multivariate formal power series to a multivariate polynomial.
If `f : MvPowerSeries σ R` and `n : σ →₀ ℕ` is a (finitely-supported) function from `σ`
to the naturals, then `trunc' R n f` is the multivariable power series obtained from `f`
by keeping only the monomials $c\prod_i X_i^{a_i}$ where `a i ≤ n i` for all `i`. -/
def trunc' : MvPowerSeries σ R →+ MvPolynomial σ R
where
toFun := truncFun' n
map_zero' := by
ext
simp only [coeff_truncFun', map_zero, ite_self, MvPolynomial.coeff_zero]
map_add' x
y := by
ext m
simp only [coeff_truncFun', MvPolynomial.coeff_add]
rw [ite_add_ite, ← map_add, zero_add]
