swap_mul_self

Mathlib.Algebra.Group.End

URI: https://scilib.ai/kg/mathlib#Equiv.swap_mul_self

English

The inverse of the swap permutation is itself; swapping i and j is an involution.

Русский

Обратная перестановка swap i j равна самой swap i j; обмен i и j является инволюцией.

LaTeX

$$$ (\\mathrm{swap}(x,y))^{-1} = \\mathrm{swap}(x,y) $$$

Lean4

@[simp]
theorem swap_mul_self (i j : α) : swap i j * swap i j = 1 :=
  swap_swap i j

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

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

Разделы

Аффилиация

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