instAlgebraPowerSeries — Mathlib

English

There is an algebra structure on LaurentSeries R coming from the algebra of PowerSeries R, i.e., LaurentSeries R is equipped with an R-algebra structure induced by HahnSeries.ofPowerSeries.

Русский

У LaurentSeries R имеется структура алгебры над R, полученная от алгебры PowerSeries R через HahnSeries.ofPowerSeries.

LaTeX

$$$\text{LaurentSeries}_R \text{ carries an } \mathsf{Algebra}_R\big(\text{PowerSeries } R\big)$-structure$$

Lean4

instance [CommSemiring R] : Algebra R⟦X⟧ R⸨X⸩ :=
  (HahnSeries.ofPowerSeries ℤ R).toAlgebra

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