truncFun' — Mathlib

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 φ)

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