algebraMvPolynomial — Mathlib

English

There is an algebra structure on MvPowerSeries over MvPolynomial, i.e., an Algebra (MvPolynomial σ R) (MvPowerSeries σ A).

Русский

Существует структура алгебры на MvPowerSeries над MvPolynomial, то есть Algebra (MvPolynomial σ R) (MvPowerSeries σ A).

LaTeX

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

Lean4

instance algebraMvPolynomial : Algebra (MvPolynomial σ R) (MvPowerSeries σ A) :=
  RingHom.toAlgebra (MvPolynomial.coeToMvPowerSeries.algHom A).toRingHom

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