coeff_truncFun — Mathlib

English

Substituting and then truncating yields the polynomial whose coefficients agree with the original up to the truncation level.

Русский

После подстановки и усечения коэффициенты совпадают с исходными до заданного уровня усечения.

LaTeX

$$$\operatorname{trunc}(n) \circ \operatorname{subst}(a) = \operatorname{trunc}(n)\,\text{composition}$$$

Lean4

theorem coeff_truncFun (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : (truncFun n φ).coeff m = if m < n then coeff m φ else 0 :=
  by classical simp [truncFun, MvPolynomial.coeff_sum]

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