English
If f is a cycle, its order is prime, and 0 < n < orderOf f, then f^n is a cycle.
Русский
Если orderOf f прост, и 0 < n < orderOf f, то f^n — это цикл.
LaTeX
$$$\\forall f : \\mathrm{Perm}(\\beta),\\; \\mathrm{IsCycle}(f) \\land \\mathrm{orderOf}(f) \\text{ is prime} \\land 0 < n < \\mathrm{orderOf}(f) \\Rightarrow \\mathrm{IsCycle}(f^n).$$$
Lean4
theorem isConj_iff (hσ : IsCycle σ) (hτ : IsCycle τ) : IsConj σ τ ↔ #σ.support = #τ.support
where
mp
h := by
obtain ⟨π, rfl⟩ := (_root_.isConj_iff).1 h
refine
Finset.card_bij (fun a _ => π a) (fun _ ha => ?_) (fun _ _ _ _ ab => π.injective ab) fun b hb ↦
⟨π⁻¹ b, ?_, π.apply_inv_self b⟩
· simp [mem_support.1 ha]
contrapose! hb
rw [mem_support, Classical.not_not] at hb
rw [mem_support, Classical.not_not, Perm.mul_apply, Perm.mul_apply, hb, Perm.apply_inv_self]
mpr := hσ.isConj hτ
