toEnd — Mathlib

English

The End construction gives a monoid of endomorphisms; End is the monoid (A →ₐ[R] A) under composition.

Русский

Конструкция End образует моноид эндоморфизмов; End — моноид (A →ₐ[R] A) по композиции.

LaTeX

$$$$ \text{End} = (A \toₐ[R] A, \circ, \mathrm{id}_A) \text{ is a monoid}. $$$$

Lean4

/-- `AlgHom.toLinearMap` as a `MonoidHom`. -/
@[simps]
def toEnd : (A →ₐ[R] A) →* Module.End R A where
  toFun := toLinearMap
  map_one' := rfl
  map_mul' _ _ := rfl

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