smulCommClass_right

Mathlib.GroupTheory.Submonoid.Center

URI: https://scilib.ai/kg/mathlib#Submonoid.center.smulCommClass_right

← MathLib Explorer

English

The center of a monoid also acts commutatively on M from the right (via symmetry).

Русский

Центр моноида также действует коммутативно на M справа (через симметрию).

LaTeX

$$SMulCommClass M (center M) M$$

Lean4

/-- The center of a monoid acts commutatively on that monoid. -/
instance smulCommClass_right : SMulCommClass M (center M) M :=
  SMulCommClass.symm _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru