English
The truncation-truncFun' of φ yields the coefficient at m as if m ≤ n then coeff m φ else 0.
Русский
Коэффициенты усечения через трuncatedFun' удовлетворяют: если m ≤ n, то coeff m φ, иначе 0.
LaTeX
$$$$ (\\operatorname{truncFun}' n \\varphi)_{m} = \\begin{cases} \\operatorname{coeff}_{m}(\\varphi), & m \\le n \\\\ 0, & \\text{otherwise} \\end{cases} $$$$
Lean4
/-- Auxiliary definition for the truncation function. -/
def truncFun' (φ : MvPowerSeries σ R) : MvPolynomial σ R :=
∑ m ∈ Finset.Iic n, MvPolynomial.monomial m (coeff m φ)