English
The polynomial algebra MvPolynomial σ S1 carries a distributive scalar action of R: for all r in R and p, q in MvPolynomial σ S1, r • (p + q) = r • p + r • q and (r s) • p = r • (s • p).
Русский
Алгебра полиномов MvPolynomial σ S1 имеет распределённое действие скаляра из R: для всех r∈R и p, q∈MvPolynomial σ S1 выполняются равенства r • (p + q) = r • p + r • q и (r s) • p = r • (s • p).
LaTeX
$$$ \text{DistribMulAction}_R(\,MvPolynomial(\,σ, S1)\, ), $$$
Lean4
instance distribuMulAction [Monoid R] [CommSemiring S₁] [DistribMulAction R S₁] :
DistribMulAction R (MvPolynomial σ S₁) :=
AddMonoidAlgebra.distribMulAction