smulCommClass_left — Mathlib

English

The center of a monoid acts commutatively on that monoid from the left; formalized as an SMulCommClass instance.

Русский

Центр моноида действует на этот моноид слева в виде объекта SMulCommClass.

LaTeX

$$SMulCommClass (center M) M M$$

Lean4

/-- The center of a monoid acts commutatively on that monoid. -/
instance smulCommClass_left : SMulCommClass (center M) M M where smul_comm m x y := Commute.left_comm (m.prop.comm x) y

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