monoid — Mathlib

English

End X forms a monoid under composition in any category.

Русский

Эндоморфизмы объекта X образуют моноид относительно композиции.

LaTeX

$$$\mathrm{End}(X) \text{ верно образуется как моноид under }\circ$$$

Lean4

/-- Endomorphisms of an object form a monoid -/
instance monoid {C : Type u} [Category.{v} C] {X : C} : Monoid (End X)
    where
  mul_one := Category.id_comp
  one_mul := Category.comp_id
  mul_assoc := fun x y z => (Category.assoc z y x).symm

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