coeff_toMvPowerSeries — Mathlib

English

For f in HahnSeries with finite index, the coefficient at n in the image under the isomorphism toMvPowerSeries equals the original coefficient at n.

Русский

Для массива f в рядах Хана с конечным индексом, коэффициент при n после перехода через изоморфизм toMvPowerSeries равен исходному коэффициенту при n.

LaTeX

$$$\\operatorname{MvPowerSeries}.\\mathrm{coeff}_{n}(\\mathrm{toMvPowerSeries}(f)) = f.\\mathrm{coeff}_{n}$$$

Lean4

theorem coeff_toMvPowerSeries {f : HahnSeries (σ →₀ ℕ) R} {n : σ →₀ ℕ} :
    MvPowerSeries.coeff n (toMvPowerSeries f) = f.coeff n :=
  rfl

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