coe_monoidHom_symm_comp_coe_monoidHom

Mathlib.Algebra.Group.Equiv.Defs

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

English

The composition in the opposite order also yields the identity: e^{-1} ∘ e = id_M.

Русский

Обратная последовательность даёт тождество: e^{-1} ∘ e = id_M.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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