instSemigroup — Mathlib

English

The product of two semigroups is a semigroup, i.e., multiplication in M × N is associative: ((a,b)·(c,d))·(e,f) = (a,b)·((c,d)·(e,f)).

Русский

Произведение полугрупп является полугруппой: ассоциативность умножения в M × N: ((a,b)·(c,d))·(e,f) = (a,b)·((c,d)·(e,f)).

LaTeX

$$$((a,b)\cdot (c,d))\cdot (e,f) = (a,b)\cdot((c,d)\cdot (e,f))$$$

Lean4

@[to_additive]
instance instSemigroup [Semigroup M] [Semigroup N] : Semigroup (M × N) where
  mul_assoc _ _ _ := by ext <;> exact mul_assoc ..

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