instSemigroup — Mathlib

English

If M is a semigroup, then Germ l M is a semigroup with multiplication defined pointwise via map₂.

Русский

Если M — полугруппа, то Germ l M — полугруппа, умножение определяется по точкам через map₂.

LaTeX

$$$ \\text{instSemigroup }[\\text{Semigroup } M] : \\text{Semigroup } (\\mathrm{Germ}(l, M)) $$$

Lean4

@[to_additive]
instance instSemigroup [Semigroup M] : Semigroup (Germ l M) :=
  { mul_assoc := fun a b c => Quotient.inductionOn₃' a b c fun _ _ _ => congrArg ofFun <| mul_assoc .. }

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