End — Mathlib

English

The endomorphisms of a bialgebra form a monoid under composition, with the identity map as the unit.

Русский

Эндоморфизмы биалгебры образуют моноид по композиции, единичный предел служит единицей.

LaTeX

$$$(\mathrm{End}_{R}(A), \circ, \mathrm{id}_{A})$ является моидом.$$

Lean4

@[simps -isSimp toSemigroup_toMul_mul toOne_one]
instance End : Monoid (A →ₐc[R] A) where
  mul := comp
  mul_assoc _ _ _ := rfl
  one := BialgHom.id R A
  one_mul _ := ext fun _ => rfl
  mul_one _ := ext fun _ => rfl

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