instMonoid — Mathlib

English

The endomorphisms α →+* α form a monoid under composition, with identity map as the unit.

Русский

Множество концевых гомоморфизмов α →+* α образует моноид при композиции, единичный гомоморфизм служит единицей.

LaTeX

$$\mathrm{End}(\alpha) \text{ is a monoid under composition with } \mathrm{id}_\alpha as identity.$$

Lean4

instance instMonoid : Monoid (α →+* α) where
  mul_one := comp_id
  one_mul := id_comp
  mul_assoc _ _ _ := comp_assoc _ _ _
  npow n f := (npowRec n f).copy f^[n] <| by induction n <;> simp [npowRec, *]
  npow_succ _ _ := DFunLike.coe_injective <| Function.iterate_succ _ _

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