coe_monoidHom_comp_coe_monoidHom_symm

Mathlib.Algebra.Group.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm

English

The composition of a monoid isomorphism with its inverse is the identity.

Русский

Составление моноид-омонима с его обратным даёт тождество.

LaTeX

$$$$ (\operatorname{toMonoidHom} e) \circ (\operatorname{toMonoidHom} e)^{-1} = \mathrm{id}_{N}. $$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_monoidHom_comp_coe_monoidHom_symm (e : M ≃* N) : (e : M →* N).comp e.symm = MonoidHom.id _ := by ext; simp

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

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

Разделы

Аффилиация

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