algebraMvPowerSeries — Mathlib

English

The same algebraic relation as a type-class instance: an algebra structure on MvPowerSeries with the given parameters.

Русский

Та же алгебраическая связь как инстанс: алгебра над MvPowerSeries с заданными параметрами.

LaTeX

$$$\\text{Algebra}(\\mathrm{MvPolynomial}_{\\sigma} R, \\mathrm{MvPowerSeries}_{\\sigma} A)$$$

Lean4

instance algebraMvPowerSeries : Algebra (MvPowerSeries σ R) (MvPowerSeries σ A) :=
  (map (algebraMap R A)).toAlgebra

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