English
Let f be a cyclic permutation on the set α. If x is moved by f (i.e., f(x) ≠ x) and f^2(x) = x, then f is the transposition swapping x with f(x).
Русский
Пусть f — цикл в группе перестановок на A. Если x не фиксирован f (f(x) ≠ x) и f^2(x) = x, то f — транспозиция, меняющая местами x и f(x).
LaTeX
$$$\operatorname{IsCycle}(f) \wedge f(x) \neq x \wedge f(f(x)) = x \Rightarrow f = \mathrm{swap}(x, f(x))$$$
Lean4
theorem eq_swap_of_apply_apply_eq_self {α : Type*} [DecidableEq α] {f : Perm α} (hf : IsCycle f) {x : α} (hfx : f x ≠ x)
(hffx : f (f x) = x) : f = swap x (f x) :=
Equiv.ext fun y =>
let ⟨z, hz⟩ := hf
let ⟨i, hi⟩ := hz.2 hfx
if hyx : y = x then by simp [hyx]
else
if hfyx : y = f x then by simp [hfyx, hffx]
else by
rw [swap_apply_of_ne_of_ne hyx hfyx]
refine by_contradiction fun hy => ?_
obtain ⟨j, hj⟩ := hz.2 hy
rw [← sub_add_cancel j i, zpow_add, mul_apply, hi] at hj
rcases zpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji | hji
· rw [← hj, hji] at hyx
tauto
· rw [← hj, hji] at hfyx
tauto
