coeff_trunc' — Mathlib

English

The coefficient of trunc' R n φ at m is equal to coeff m φ if m ≤ n, otherwise 0.

Русский

Коэффициент усечения' R n φ в позиции m равен coeff m φ, если m ≤ n, иначе 0.

LaTeX

$$$$ (\\operatorname{coeff}_{m}(\\operatorname{trunc'} R n \\varphi)) = \\begin{cases} \\operatorname{coeff}_{m}(\\varphi), & m \\le n \\\\ 0, & \\text{otherwise} \\end{cases} $$$$

Lean4

/-- Coefficients of the truncation of a multivariate power series. -/
theorem coeff_trunc' (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : (trunc' R n φ).coeff m = if m ≤ n then coeff m φ else 0 :=
  coeff_truncFun' n m φ

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