instSMulCommClass — Mathlib

English

If scalar actions commute suitably, Unitization R A has SMulCommClass with respect to the two base scalars.

Русский

При должном взаимном коммютировании действия скаляров Unitization R A имеет SMulCommClass относительно двух оснований скаляра.

LaTeX

$$$[SMul T R] [SMul T A] [SMul S R] [SMul S A] [SMulCommClass T S R] [SMulCommClass T S A] \\\\Rightarrow SMulCommClass T S (Unitization R A).$$$

Lean4

instance instSMulCommClass [SMul T R] [SMul T A] [SMul S R] [SMul S A] [SMulCommClass T S R] [SMulCommClass T S A] :
    SMulCommClass T S (Unitization R A) :=
  Prod.smulCommClass

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