instIsId

Mathlib.Algebra.Group.Hom.CompTypeclasses

URI: https://scilib.ai/kg/mathlib#MonoidHom.CompTriple.instIsId

English

For every monoid M, the identity monoid homomorphism id_M is the identity map (on M).

Русский

Для каждого моноида M тождественный моноид-гомоморфизм id_M есть тождественное отображение на M.

LaTeX

$$$$ \forall x \in M,\ id_M(x) = x. $$$$

Lean4

instance instIsId {M : Type*} [Monoid M] : IsId (MonoidHom.id M) where eq_id := rfl

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

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

Разделы

Аффилиация

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