smulCommClass_right — Mathlib

English

Under a Monoid N action and compatible actions, the smul-commutativity lifts to SMulCommClass M with Units N.

Русский

При моноиде N и совместимых действиях переносится коммутативность умножения к SMulCommClass M Nˣ α.

LaTeX

$$$ [Monoid N] [SMul M \\alpha] [SMul N \\alpha] [SMulCommClass M N \\alpha] : SMulCommClass M N^\\times \\alpha$$$

Lean4

@[to_additive]
instance smulCommClass_right [Monoid N] [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass M Nˣ α where
  smul_comm m n := smul_comm m (n : N)

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