swap_smul_self_smul — Mathlib

English

In a permutation action, swapping i and j twice acts trivially on any element x: applying the transposition twice returns to x.

Русский

При действии перестановки двойной обмен i и j действует тривиально: после двух применений к элементу x получаем исходный x.

LaTeX

$$$\\text{swap}(i,j)\\;\\text{smul}\\;\\text{swap}(i,j)\\;\\text{smul} \\; x = x$$$

Lean4

@[simp]
theorem swap_smul_self_smul [MulAction (Perm α) β] (i j : α) (x : β) : swap i j • swap i j • x = x := by
  simp [smul_smul]

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