toEnd_def

Mathlib.CategoryTheory.SingleObj

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SingleObj.toEnd_def

English

The map toEnd from the monoid M to End(SingleObj.star M) acts as the identity on elements, i.e., toEnd M x = x.

Русский

Отображение toEnd с M в End(SingleObj.star M) действует как тождественное на элементы: toEnd M x = x.

LaTeX

$$$toEnd\\;M\\;x = x$$$

Lean4

theorem toEnd_def (x : M) : toEnd M x = x :=
  rfl

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

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

Разделы

Аффилиация

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