instSMulCommClass' — Mathlib

English

Suppose there is a SMulCommClass R' R A and IsScalarTower R' R A; then the induced SMulCommClass on the subalgebra S holds: r' • (r • s) = r • (r' • s) for all r' ∈ R', r ∈ R, s ∈ S.

Русский

Пусть есть свойство SMulCommClass(R',R,A) и IsScalarTower(R',R,A); следовательно, для подпалгебры S выполняется коммутативность действий скаляров: r' • (r • s) = r • (r' • s) для всех r' ∈ R', r ∈ R, s ∈ S.

LaTeX

$$$ \\forall r' \\in R',\\ \\forall r \\in R,\\ \\forall s \\in S:\\ (r' r) \\cdot s = r' \\cdot (r \\cdot s). $$$

Lean4

instance instSMulCommClass' [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] [SMulCommClass R' R A] :
    SMulCommClass R' R S where smul_comm r' r s := Subtype.ext <| smul_comm r' r (s : A)

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