instMonoid — Mathlib

English

Endomorphisms of a star-ring (respecting addition, multiplication, and star) form a monoid under composition.

Русский

Окончательные отображения кольца со звездой образуют моноид относительно композиции.

LaTeX

$$$ (f \circ g)(x) = f(g(x)) \quad\text{and}\quad \mathrm{id} \circ f = f = f \circ \mathrm{id} $$$

Lean4

instance : Monoid (A →⋆ₙ+* A) where
  mul := comp
  mul_assoc := comp_assoc
  one := NonUnitalStarRingHom.id A
  one_mul := id_comp
  mul_one := comp_id

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