English
If f is a cycle on α, and x is moved by f with f^2(x) ≠ x, then the permutation swap x with f(x) left-multiplied by f is again a cycle.
Русский
Если f — цикл на α, и x перемещается элементом f при условии f^2(x) ≠ x, тогда произведение слева транспозиции swap(x, f(x)) и f является снова циклической перестановкой.
LaTeX
$$$\operatorname{IsCycle}(f) \wedge f(x) \neq x \wedge f(f(x)) \neq x \Rightarrow \operatorname{IsCycle}(\mathrm{swap}(x, f(x)) \cdot f)$$$
Lean4
theorem swap_mul {α : Type*} [DecidableEq α] {f : Perm α} (hf : IsCycle f) {x : α} (hx : f x ≠ x) (hffx : f (f x) ≠ x) :
IsCycle (swap x (f x) * f) :=
⟨f x, by simp [swap_apply_def, mul_apply, if_neg hffx, f.injective.eq_iff, hx], fun y hy =>
let ⟨i, hi⟩ := hf.exists_zpow_eq hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1
have hi : (f ^ (i - 1)) (f x) = y :=
calc
(f ^ (i - 1) : Perm α) (f x) = (f ^ (i - 1) * f ^ (1 : ℤ) : Perm α) x := by simp
_ = y := by rwa [← zpow_add, sub_add_cancel]
isCycle_swap_mul_aux₂ (i - 1) hy hi⟩
