powerSeriesAlgebra — Mathlib

English

Casting a power series as a Hahn series yields an algebra structure over S, transported via the canonical maps: Algebra S (PowerSeries R) to Algebra S (HahnSeries Γ R).

Русский

Переход степенного ряда в ряд Хана порождает алгебраическую структуру над S, переносимую по каноническим отображениям: Algebra S (PowerSeries R) → Algebra S (HahnSeries Γ R).

LaTeX

$$$\\text{powerSeriesAlgebra}$ : \\ Algebra S (HahnSeries Γ R)$ is defined by $(a, f) \\mapsto \\mathrm{ofPowerSeries}_{\\Gamma,R}(\\mathrm{algebraMap}_S(\\mathrm{PowerSeries} R)(a)) \\cdot f$$$

Lean4

instance powerSeriesAlgebra {S : Type*} [CommSemiring S] [Algebra S (PowerSeries R)] : Algebra S (HahnSeries Γ R) :=
  RingHom.toAlgebra <| (ofPowerSeries Γ R).comp (algebraMap S (PowerSeries R))

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