semigroup — Mathlib

English

If α is a semigroup, then Set α is a semigroup under pointwise multiplication.

Русский

Если α образует полугруппа, то Set α образует полугруппу под точечным умножением.

LaTeX

$$$$ (S * T) * U = S * (T * U). $$$$

Lean4

/-- `Set α` is a `Semigroup` under pointwise operations if `α` is. -/
@[to_additive /-- `Set α` is an `AddSemigroup` under pointwise operations if `α` is. -/
    ]
protected def semigroup [Semigroup α] : Semigroup (Set α) :=
  { Set.mul with mul_assoc := fun _ _ _ => image2_assoc mul_assoc }

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