LaurentSeriesRingEquiv_def — Mathlib

English

The action of the LaurentSeriesRingEquiv on a power series f is given by the compare map against ratfuncAdicComplPkg.

Русский

Действие LaurentSeriesRingEquiv на ряд мощности f задано через отображение compare против ratfuncAdicComplPkg.

LaTeX

$$$(\\mathrm{LaurentSeriesRingEquiv}\\,K)\\,f = (\\mathrm{LaurentSeriesPkg}\\,K).\\mathrm{compare}\\ \\mathrm{ratfuncAdicComplPkg}\\,(f) $$$

Lean4

@[simp]
theorem LaurentSeriesRingEquiv_def (f : K⟦X⟧) :
    (LaurentSeriesRingEquiv K) f = (LaurentSeriesPkg K).compare ratfuncAdicComplPkg (f : K⸨X⸩) :=
  rfl

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