distribuMulAction — Mathlib

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

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