instMonoid — Mathlib

English

The End(M) endowed with composition and identity forms a monoid.

Русский

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

LaTeX

$$$\\operatorname{End}(M)\\text{ is a Monoid with } (f*g)=f\\circ g\\text{ and } 1=\\mathrm{id}_M.$$$

Lean4

@[to_additive instMonoid]
instance instMonoid : Monoid (Monoid.End M) where
  mul := MonoidHom.comp
  one := MonoidHom.id M
  mul_assoc _ _ _ := MonoidHom.comp_assoc _ _ _
  mul_one := MonoidHom.comp_id
  one_mul := MonoidHom.id_comp
  npow n f := (npowRec n f).copy f^[n] <| by induction n <;> simp [npowRec, *] <;> rfl
  npow_succ _ _ := DFunLike.coe_injective <| Function.iterate_succ _ _

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