smulCommClass_self — Mathlib

English

If M is a commutative monoid acting on α, then SMulCommClass M M α holds; actions of M on α commute with each other.

Русский

Если M — коммутативный моноид, действующий на α, то SMulCommClass M M α выполняется; действия M на α коммутируют друг с другом.

LaTeX

$$$ \text{If } M \text{ is commutative, then } a \cdot (b \cdot x) = b \cdot (a \cdot x) \text{ for all } a,b \in M, x \in α.$$$

Lean4

@[to_additive]
instance smulCommClass_self (M α : Type*) [CommMonoid M] [MulAction M α] : SMulCommClass M M α where
  smul_comm a a' b := by rw [← mul_smul, mul_comm, mul_smul]

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