symm_trans_self

Mathlib.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#AlgEquiv.symm_trans_self

English

The symmetric map e.symm is a left inverse of e.

Русский

Симм мапа является левым обратным к исходному отображению.

LaTeX

$$$\text{LeftInverse}(e^{\mathrm{symm}}, e)$$$

Lean4

@[simp]
theorem symm_trans_self (e : A₁ ≃ₐ[R] A₂) : e.symm.trans e = refl := by ext; simp

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

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

Разделы

Аффилиация

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