instSemigroup

Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

URI: https://scilib.ai/kg/mathlib#SubMulAction.instSemigroup

English

The semigroup operation is associative; hence SubMulAction R M is a semigroup.

Русский

Операция умножения ассоциативна; следовательно SubMulAction R M является полугруппой.

LaTeX

$$$ (p * q) * r = p * (q * r) $ for all p,q,r in SubMulAction R M.$$

Lean4

instance : Semigroup (SubMulAction R M) where
  mul := (· * ·)
  mul_assoc _ _ _ := SetLike.coe_injective (mul_assoc (_ : Set _) _ _)

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

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

Разделы

Аффилиация

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