self_trans_symm

Mathlib.Algebra.Algebra.Equiv

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

English

The symmetric transposition of an algebra equivalence with itself is the identity: e.symm.trans e = refl.

Русский

Симметричная транспозиция эквивалентности с самой собой равна тождеству.

LaTeX

$$$e^{\mathrm{symm}} \mathrm{.trans} e = \mathrm{refl}$$$

Lean4

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

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

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

Разделы

Аффилиация

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