mul_swap_eq_swap_mul — Mathlib

English

Left-multiplying by swap i j is compatible with right multiplication by the inverse-conjugate of f; this expresses a standard conjugation relation.

Русский

Левостороннее умножение на swap i j совместимо с правым умножением на сопряжение через f^{-1}.

LaTeX

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

Lean4

theorem mul_swap_eq_swap_mul (f : Perm α) (x y : α) : f * swap x y = swap (f x) (f y) * f := by
  rw [swap_mul_eq_mul_swap, Perm.inv_apply_self, Perm.inv_apply_self]

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