English
Let f be a permutation of a finite set and n an integer. 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 — перестановка конечного множества и n — целое число. Если f^n — цикл и поддержка f ⊆ поддержка f^n, тогда f — цикл.
LaTeX
$$$\\forall \\alpha, \\forall f : \\mathrm{Perm}(\\alpha), \\forall n \\in \\mathbb{Z},\\; \\big( \\mathrm{IsCycle}(f^n) \\land \\mathrm{supp}(f) \\subseteq \\mathrm{supp}(f^n) \\big) \\Rightarrow \\mathrm{IsCycle}(f).$$$
Lean4
theorem of_zpow {n : ℤ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) : IsCycle f :=
by
cases n
· exact h1.of_pow h2
· simp only [zpow_negSucc, Perm.support_inv] at h1 h2
exact (inv_inv (f ^ _) ▸ h1.inv).of_pow h2
