instMonoid — Mathlib

English

The endomorphism ring End_R(M) forms a Monoid under composition, with 1 as the identity and multiplication given by composition.

Русский

Кольцо эндоморфизмов End_R(M) образует моноид по композиции: единица — идентичность, умножение — композиция.

LaTeX

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

Lean4

instance instMonoid : Monoid (Module.End R M)
    where
  mul_assoc _ _ _ := LinearMap.ext fun _ ↦ rfl
  mul_one := comp_id
  one_mul := id_comp

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