instMonoid — Mathlib

English

The endomorphisms A →⋆* A form a monoid under composition, with identity given by the identity star-monoid homomorphism and multiplication given by composition.

Русский

Эндоморфизмы A →⋆* A образуют моноид под композицию, тождественный звёздный моноидный гомоморфизм — единица, а произведение — композиция.

LaTeX

$$$(A \\to⋆* A)$ endowed with $\\mul := \\mathrm{comp}$, $\\one := \\mathrm{id}_A$, $\\one\\_\\mathrm{mul} := \\mathrm{id\\_comp}$, $\\mul\\_\\mathrm{one} := \\mathrm{comp\_id}$ is a monoid.$$

Lean4

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

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