coeff_toMvPowerSeries_symm — Mathlib

English

The coefficient map commutes with the inverse of the isomorphism: the coefficient of (toMvPowerSeries).symm(f) at n equals the coefficient of f at n in the MvPowerSeries sense.

Русский

Коэффициентная карта сохраняется при обращении к обратной стороне изоморфизма: коэффициент у (toMvPowerSeries)^{-1}(f) при n равен коэффициенту f при n.

LaTeX

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

Lean4

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

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