instMonoid — Mathlib

English

Endomorphisms A →⋆ₙₐ[R] A form a monoid under composition with identity given by the identity homomorphism.

Русский

Эндоморфизмов A →⋆ₙₐ[R] A образуют моноид относительно композиции, единица — идентичный гомоморфизм.

LaTeX

$$End(A) with multiplication ∘ and unit id_A: (End(A), ∘, id_A) forms a monoid; associativity and identities hold.$$

Lean4

instance : Monoid (A →⋆ₙₐ[R] A) where
  mul := comp
  mul_assoc := comp_assoc
  one := NonUnitalStarAlgHom.id R A
  one_mul := id_comp
  mul_one := comp_id

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