instMonoid — Mathlib

English

The collection of AddConstMap G G a a forms a monoid under composition, with identity given by the AddConstMap corresponding to identity translation.

Русский

Область отображений AddConstMap G G a a образует моноид под композицию; тождественное отображение соответствует единице.

LaTeX

$$$\big(G \to+c[a,a] G\big) \text{ with composition is a Monoid.}$$$

Lean4

instance : Monoid (G →+c[a, a] G) :=
  DFunLike.coe_injective.monoid (M₂ := Function.End G) _ rfl (fun _ _ ↦ rfl) fun _ _ ↦ rfl

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