centerToCentroid — Mathlib

English

The center-to-centroid map sends a central element z to the centroid endomorphism L(z): a ↦ z a.

Русский

Переход центр→центроид отправляет центральный элемент z в центроид-эндоморфизм L(z): a ↦ z a.

LaTeX

$$$\mathrm{centerToCentroid}(z) (a) = z a$$$

Lean4

/-- The canonical homomorphism from the center into the centroid -/
def centerToCentroid : NonUnitalSubsemiring.center α →ₙ+* CentroidHom α :=
  NonUnitalRingHom.comp (SubsemiringClass.subtype (Subsemiring.center (CentroidHom α))).toNonUnitalRingHom
    centerToCentroidCenter

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