ofPowerSeries_apply — Mathlib

English

Coefficients commute with the isomorphism between HahnSeries and PowerSeries; the nth coefficient under the symm equivalence equals the nth coefficient of the original power series.

Русский

Коэффициенты коммутируют с изоморфизмом между HahnSeries и PowerSeries; коэффициент n при симметричном отображении равен коэффициенту n исходного степенного ряда.

LaTeX

$$$ (HahnSeries.toPowerSeries.symm\ f).coeff\ n = PowerSeries.coeff\ n f $$$

Lean4

theorem ofPowerSeries_apply (x : PowerSeries R) :
    ofPowerSeries Γ R x =
      HahnSeries.embDomain
        ⟨⟨((↑) : ℕ → Γ), Nat.strictMono_cast.injective⟩,
          by
          simp only [Function.Embedding.coeFn_mk]
          exact Nat.cast_le⟩
        (toPowerSeries.symm x) :=
  rfl

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