instAlgebra — Mathlib

English

There is a natural R-algebra structure on MvPowerSeries σ A, arising from the algebra structure on A and the coefficientwise map.

Русский

Существует естественная структура R-алгебры на MvPowerSeries σ A, возникающая из алгебраической структуры A и коэффициентного отображения.

LaTeX

$$$\\text{MvPowerSeries}(\\sigma, A) \\text{ is an } R\\text{-algebra}$$$

Lean4

instance : Algebra R (MvPowerSeries σ A)
    where
  algebraMap := (MvPowerSeries.map (algebraMap R A)).comp C
  commutes' := fun a φ => by
    ext n
    simp [Algebra.commutes]
  smul_def' := fun a σ => by
    ext n
    simp [(coeff A n).map_smul_of_tower a, Algebra.smul_def]

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