instOne

Mathlib.Algebra.Group.Hom.Defs

URI: https://scilib.ai/kg/mathlib#Monoid.End.instOne

English

There exists a distinguished identity endomorphism in End(M), given by the identity map on M.

Русский

Существует выделенный единичный эндоморфизм в End(M), задаваемый тождественным отображением на M.

LaTeX

$$$1_{\\operatorname{End}(M)} = \\mathrm{id}_M$.$$

Lean4

@[to_additive instOne]
instance instOne : One (Monoid.End M) where one := .id _

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

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

Разделы

Аффилиация

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