swap_mul_self_mul — Mathlib

English

Left-multiplying a permutation by swap i j twice yields the original permutation; swapping twice returns to the starting point.

Русский

Умножение слева на swap i j два раза возвращает исходную перестановку; обмен дважды возвращает исходное.

LaTeX

$$$ \\mathrm{swap}(i,j) \\cdot \\mathrm{swap}(i,j) = 1 $$$

Lean4

/-- Left-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 swap_mul_self_mul (i j : α) (σ : Perm α) : Equiv.swap i j * (Equiv.swap i j * σ) = σ := by simp [← mul_assoc]

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