powerSeriesEquivSubring_apply — Mathlib

English

For any x in RatFuncAdicCompl K, the apply of ratfuncAdicComplRingEquiv K to x equals its image under ratfuncAdicComplPkg.compare with LaurentSeriesPkg.

Русский

Для любого x из RatFuncAdicCompl K применение ratfuncAdicComplRingEquiv K к x равно образу x через ratfuncAdicComplPkg.compare с LaurentSeriesPkg.

LaTeX

$$$\\mathrm{ratfuncAdicComplRingEquiv}\\,K\\;x = \\mathrm{ratfuncAdicComplPkg}.\\mathrm{compare}\\bigl(\\mathrm{LaurentSeriesPkg}\\,K\\bigr)\\;x$$$

Lean4

theorem powerSeriesEquivSubring_apply (f : K⟦X⟧) :
    powerSeriesEquivSubring K f = ⟨HahnSeries.ofPowerSeries ℤ K f, Subring.mem_map.mpr ⟨f, trivial, rfl⟩⟩ :=
  rfl

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