coeff_trunc — Mathlib

English

The m-th coefficient of trunc n φ is equal to φ's m-th coefficient if m < n, and 0 otherwise.

Русский

Коэффициент m у trunc n φ равен коэффициенту φ_m, если m < n, иначе равен 0.

LaTeX

$$$(\\text{PowerSeries.trunc}\\ n\\ φ).\\mathrm{coeff}_m = \\begin{cases} \\mathrm{coeff}_m φ, & m < n \\\\ 0, & \\text{otherwise} \\end{cases}$$$

Lean4

theorem coeff_trunc (m) (n) (φ : R⟦X⟧) : (trunc n φ).coeff m = if m < n then coeff m φ else 0 := by
  simp [trunc, Polynomial.coeff_monomial]

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