Aut_mul_def

Mathlib.CategoryTheory.Endomorphism

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Aut.Aut_mul_def

English

Inclusion of Aut X into End X as a monoid hom.

Русский

Включение Aut X в End X как моноид-гомоморфизм.

LaTeX

$$$\text{toEnd}(X): Aut(X) \to\ End(X)$$$

Lean4

theorem Aut_mul_def (f g : Aut X) : f * g = g.trans f :=
  rfl

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

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

Разделы

Аффилиация

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