English
A technical lemma giving existence of an integral power i such that a certain conjugated swapped-multiply map sends f x to b, used in cycle arguments.
Русский
Техническая лемма, дает существование целевой степени i, чтобы некоторая композиция, включающая обмен и умножение, отправляет f x в b, используется в доказательствах циклов.
LaTeX
$$isCycle_swap_mul_aux₁ {α} [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$$
Lean4
theorem isCycle_swap (hxy : x ≠ y) : IsCycle (swap x y) :=
⟨y, by rwa [swap_apply_right], fun a (ha : ite (a = x) y (ite (a = y) x a) ≠ a) =>
if hya : y = a then ⟨0, hya⟩
else
⟨1, by
rw [zpow_one, swap_apply_def]
split_ifs at * <;> tauto⟩⟩
