End

Mathlib.LinearAlgebra.RootSystem.Hom

URI: https://scilib.ai/kg/mathlib#RootPairing.End

English

The endomorphism set End P forms a monoid under composition with identity id_P as unit.

Русский

Конечное множество End P образует моноид по конъюгации, нейтральный элемент — id_P.

LaTeX

$$Monoid (End P)$$

Lean4

/-- The endomorphism monoid of a root pairing. -/
abbrev _root_.RootPairing.End (P : RootPairing ι R M N) :=
  Hom P P

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru