to_isAssociative

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#Semigroup.to_isAssociative

English

In any semigroup (A, ·), the binary operation is associative: (a · b) · c = a · (b · c) for all a,b,c ∈ A.

Русский

В любой полугруппе (A, ·) бинарная операция ассоциативна: (a · b) · c = a · (b · c) для всех a,b,c ∈ A.

LaTeX

$$$ (a \cdot b) \cdot c = a \cdot (b \cdot c) $$$

Lean4

@[to_additive]
instance to_isAssociative : Std.Associative (α := α) (· * ·) :=
  ⟨mul_assoc⟩

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

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

Разделы

Аффилиация

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