smulCommClass — Mathlib

English

If T and S act on R and M with compatibility, then TrivSqZeroExt R M inherits a SMulCommClass T S structure.

Русский

Если T и S действуют на R и M с совместимостью, то TrivSqZeroExt R M наследует структуру SMulCommClass T S.

LaTeX

$$SMulCommClass T S (tsze R M)$$

Lean4

instance smulCommClass [SMul T R] [SMul T M] [SMul S R] [SMul S M] [SMulCommClass T S R] [SMulCommClass T S M] :
    SMulCommClass T S (tsze R M) :=
  Prod.smulCommClass

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