self_comp_symm

Mathlib.Topology.Algebra.ContinuousMonoidHom

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

English

Let e: M ≃ₜ* N. Then e ∘ e^{-1} = id on N; the composition of e with its inverse is the identity on N.

Русский

Пусть e: M ≃ₜ* N. Тогда e ∘ e^{-1} = id на N; композиция e с её обратным — тождество на N.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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