instSMulCommClass — Mathlib

English

If R,S,A are commutative semirings with A an R- and S-algebra and SMul R S (FreeAlgebra A X) holds, then FreeAlgebra has SMulCommClass R S.

Русский

Пусть R,S,A — коммутативные полукольца, A — R-алгебра и S-алгебра, и существует SMulCommClass R S (FreeAlgebra A X). Тогда FreeAlgebra имеет SMulCommClass R S.

LaTeX

$$$\mathrm{SMulCommClass}\; R\ S\; (\mathrm{FreeAlgebra}(A,X)).$$$

Lean4

instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A] [Algebra R A] [Algebra S A] :
    SMulCommClass R S (FreeAlgebra A X) where smul_comm r s x := smul_comm (algebraMap R A r) (algebraMap S A s) x

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