mul_swap_mul_self — Mathlib

English

Multiplying on the right by a swap is an involution, mirroring the left-involutive property of swapping twice.

Русский

Правое умножение на swap является инволюцией, аналогично левой инволютности перестановки.

LaTeX

$$A function x ↦ x · swap(i,j) is involutive, i.e. (x·swap(i,j))·swap(i,j) = x for all x.$$

Lean4

/-- Right-multiplying a permutation with `swap i j` twice gives the original permutation.

  This specialization of `swap_mul_self` is useful when using cosets of permutations.
-/
@[simp]
theorem mul_swap_mul_self (i j : α) (σ : Perm α) : σ * Equiv.swap i j * Equiv.swap i j = σ := by
  rw [mul_assoc, swap_mul_self, mul_one]

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