swap_apply_apply

Mathlib.Algebra.Group.End

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

English

Applying a swap and then its inverse is the identity, reflecting that a swap is an involution.

Русский

Применение обмена и его обратного равно единице; обмен — инволюция.

LaTeX

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

Lean4

theorem swap_apply_apply (f : Perm α) (x y : α) : swap (f x) (f y) = f * swap x y * f⁻¹ := by
  rw [mul_swap_eq_swap_mul, mul_inv_cancel_right]

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

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

Разделы

Аффилиация

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