ofPowerSeries_apply_coeff — Mathlib

English

For x in PowerSeries R, the coeff of (ofPowerSeries Γ R x) at n equals the nth coefficient of x.

Русский

Для x в PowerSeries R коэффициент при n у (ofPowerSeries Γ R x) равен n-му коэффициенту x.

LaTeX

$$$ (\mathrm{ofPowerSeries}\ \Gamma\ R\ x).\coeff\ n = \mathrm{PowerSeries.coeff}\ n x $$$

Lean4

theorem ofPowerSeries_apply_coeff (x : PowerSeries R) (n : ℕ) : (ofPowerSeries Γ R x).coeff n = PowerSeries.coeff n x :=
  by simp [ofPowerSeries_apply]

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