instSMulCommClass — Mathlib

English

If A,B are AddZeroClass, then SMulCommClass M N (A →+ B) holds given DistribSMul M B, DistribSMul N B and SMulCommClass M N B.

Русский

Если A,B — дополнительно нулевые группы, то выполняется SMulCommClass M N (A →+ B) при условии DistribSMul M B, DistribSMul N B и SMulCommClass M N B.

LaTeX

$$[DistribSMul M B] [DistribSMul N B] [SMulCommClass M N B] : SMulCommClass M N (A →+ B)$$

Lean4

instance [DistribSMul M B] [DistribSMul N B] [SMulCommClass M N B] : SMulCommClass M N (A →+ B) where
  smul_comm _ _ _ := ext fun _ => smul_comm _ _ _

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