symm_comp_self

Mathlib.Topology.Algebra.Algebra.Equiv

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

English

The composition of the inverse with the original is the identity on A: (e.symm : B → A) ∘ e = id_A.

Русский

Сложение обратной карты с исходной дает тождество на A: (e.symm ∘ e) = id_A.

LaTeX

$$$(e^{\mathrm{symm}}) \circ e = \mathrm{id}_A$$$

Lean4

@[simp]
theorem symm_comp_self (e : A ≃A[R] B) : (e.symm : B → A) ∘ e = id := by exact funext <| e.symm_apply_apply

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

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

Разделы

Аффилиация

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