End — Mathlib

English

The endomorphisms of A form a monoid under composition, with identity being id and multiplication given by composition.

Русский

Эндоморфизмы A образуют моноид при композиции; единица — это id, умножение — композиция.

LaTeX

$$$$(\mathrm{AlgHom}(R,A,A), \circ, \mathrm{id}_A) \text{ is a monoid.}$$$$

Lean4

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

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