smulCommClass_left — Mathlib

English

Given a G-action on M and a compatible action on N, the commutativity of smul lifts to the Units M acting on N.

Русский

При наличии действия G на M и совместимого действия на N коммутативность скалярного умножения поднимается на Units M acting on N.

LaTeX

$$$ [Monoid M] [SMul M \\alpha] [SMul N \\alpha] [SMulCommClass M N \\alpha] : SMulCommClass (Units M) N \\alpha$$$

Lean4

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

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