coeff_coe — Mathlib

English

For any n, the n-th coefficient of φ viewed as a power series equals φ’s n-th coefficient.

Русский

Для любого n-ого коэффициента: коэффициент n у φ, воспринятого как ряд, равен n-ому коэффициенту φ.

LaTeX

$$$\\operatorname{PowerSeries.coeff} n \\varphi = \\operatorname{coeff}(\\varphi,n)$$$

Lean4

@[simp, norm_cast]
theorem coeff_coe (n) : PowerSeries.coeff n φ = coeff φ n :=
  congr_arg (coeff φ) Finsupp.single_eq_same

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