symm_trans_self

Mathlib.Algebra.Lie.Basic

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

English

Symmetry is involutive: applying symmetry twice yields the original.

Русский

Симметрия является инволютивной: применение симметрии дважды возвращает исходное.

LaTeX

$$$e^{\\mathrm{symm}}(e(x)) = x$$$

Lean4

@[simp]
theorem symm_trans_self (e : M ≃ₗ⁅R,L⁆ N) : e.symm.trans e = refl :=
  ext _ _ e.apply_symm_apply

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

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

Разделы

Аффилиация

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