swap_mul_swap_mul_swap — Mathlib

English

For x,y,z ∈ α with x ≠ y and x ≠ z, the product of transpositions (y z)(x y)(y z) equals (z x).

Русский

Для элементов x,y,z ∈ α с условиями x ≠ y и x ≠ z выполняется (y z)(x y)(y z) = (z x).

LaTeX

$$$$ x,y,z \in \\alpha,\\ (x \\neq y) \\land (x \\neq z) \\Rightarrow (y\\, z)(x\\, y)(y\\, z) = (z\\, x). $$$$

Lean4

theorem swap_mul_swap_mul_swap {x y z : α} (hxy : x ≠ y) (hxz : x ≠ z) : swap y z * swap x y * swap y z = swap z x :=
  by
  nth_rewrite 3 [← swap_inv]
  rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm]

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