English
Let f be a permutation on α. If f^n is a cycle and the support of f is contained in the support of f^n, then f is a cycle.
Русский
Пусть f — перестановка на α. Если f^n является циклом и поддержка f ⊆ поддержка f^n, то и f является циклом.
LaTeX
$$$((f^n)\\ \\text{is a cycle}) \\wedge (\\operatorname{supp}(f) \\subseteq \\operatorname{supp}(f^n)) \\Rightarrow \\operatorname{IsCycle}(f)$$
Lean4
theorem of_pow {n : ℕ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) : IsCycle f :=
by
have key : ∀ x : α, (f ^ n) x ≠ x ↔ f x ≠ x :=
by
simp_rw [← mem_support, ← Finset.ext_iff]
exact (support_pow_le _ n).antisymm h2
obtain ⟨x, hx1, hx2⟩ := h1
refine ⟨x, (key x).mp hx1, fun y hy => ?_⟩
obtain ⟨i, _⟩ := hx2 ((key y).mpr hy)
exact
⟨n * i, by rwa [zpow_mul]⟩
-- The lemma `support_zpow_le` is relevant. It means that `h2` is equivalent to
-- `σ.support = (σ ^ n).support`, as well as to `#σ.support ≤ #(σ ^ n).support`.
