English
In the permutation group, under certain hypotheses about a swap and a permutation f, there exists an integer i such that the i-th power of the composed permutation sends f x to b.
Русский
В группе перестановок при определённых предпосылках касательно обмена и перестановки f существует целое число i, такое что i-й порядок степени композиции отображает f x в b.
LaTeX
$$$ \\exists i \\in \\mathbb{Z}, \\; ((\\text{swap } x (f x) \\cdot f)^i)(f x) = b $$$
Lean4
theorem isCycle_swap_mul_aux₁ {α : Type*} [DecidableEq α] :
∀ (n : ℕ) {b x : α} {f : Perm α} (_ : (swap x (f x) * f) b ≠ b) (_ : (f ^ n) (f x) = b),
∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b :=
by
intro n
induction n with
| zero => exact fun _ h => ⟨0, h⟩
| succ n hn =>
intro b x f hb h
exact
if hfbx : f x = b then ⟨0, hfbx⟩
else
have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
have hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b :=
by
rw [mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx), Ne, ← f.injective.eq_iff,
apply_inv_self]
exact this.1
let ⟨i, hi⟩ := hn hb' (f.injective <| by rw [apply_inv_self]; rwa [pow_succ', mul_apply] at h)
⟨i + 1, by
rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_inv_self,
swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (Ne.symm hfbx)]⟩
