instMonoidEnd — Mathlib

English

The endomorphism monoid End(α) forms a monoid under composition.

Русский

Моноид End(α) образования отображений α в себя образует моноид под операцией композиции.

LaTeX

$$$\\\\operatorname{Monoid}(\\\\operatorname{End}(\\\\alpha))$$$

Lean4

instance : Monoid (Function.End α) where
  one := id
  mul := (· ∘ ·)
  mul_assoc _ _ _ := rfl
  mul_one _ := rfl
  one_mul _ := rfl
  npow n f := f^[n]
  npow_succ _ _ := Function.iterate_succ _ _

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