English
For a finite β and a cycle f, f^a = f^b holds iff there exists a moved point x with f^a x = f^b x and f x ≠ x.
Русский
Для цикла f в конечном β, равенство f^a = f^b эквивалентно существованию перемещаемой точки x, для которой f^a x = f^b x и f x ≠ x.
LaTeX
$$$\\forall f : \\mathrm{Equiv.Perm}(\\beta),\\; f.IsCycle \\Rightarrow \\forall a,b : \\mathrm{Nat},\\; \\; f^a = f^b \\iff \\exists x, f x \\neq x \\land (f^a) x = (f^b) x.$$$
Lean4
theorem isConj (hσ : IsCycle σ) (hτ : IsCycle τ) (h : #σ.support = #τ.support) : IsConj σ τ :=
by
refine
isConj_of_support_equiv
(hσ.zpowersEquivSupport.symm.trans <|
(zpowersEquivZPowers <| by rw [hσ.orderOf, h, hτ.orderOf]).trans hτ.zpowersEquivSupport)
?_
intro x hx
simp only [Equiv.trans_apply]
obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)
simp [← Perm.mul_apply, ← pow_succ']
