English
The coeff in the truncated polynomial equals the corresponding coeff in the original when the index is below n, otherwise zero.
Русский
Коэффициент в усечённом полиномe равен соответствующему коэффициенту в исходном, если индекс ниже n, иначе ноль.
LaTeX
$$$(\operatorname{coeff} m (\operatorname{truncFun} n \varphi)) = \begin{cases} \operatorname{coeff} m \varphi, & m < n \\ 0, & \text{otherwise} \end{cases}$$$
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`
and $a i < n i` for some `i`. -/
def trunc : MvPowerSeries σ R →+ MvPolynomial σ R
where
toFun := truncFun n
map_zero' := by
classical
ext
simp [coeff_truncFun]
map_add' := by
classical
intro x y
ext m
simp only [coeff_truncFun, MvPolynomial.coeff_add, ite_add_ite, ← map_add, add_zero]
