symm_comp_self

Mathlib.Topology.Algebra.ContinuousMonoidHom

URI: https://scilib.ai/kg/mathlib#ContinuousMulEquiv.symm_comp_self

English

Let e: M ≃ₜ* N. Then e^{-1} ∘ e = id on M, i.e., e.symm ∘ e = id_M.

Русский

Пусть e: M ≃ₜ* N. Тогда e^{-1} ∘ e = id на M, то есть e.symm ∘ e = id_M.

LaTeX

$$$e^{-1} \circ e = \mathrm{id}_M.$$$

Lean4

@[to_additive (attr := simp)]
theorem symm_comp_self (e : M ≃ₜ* N) : e.symm ∘ e = id :=
  funext e.symm_apply_apply

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

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

Разделы

Аффилиация

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