English
For a finite β and a cycle f, the support of f^n is equal to the support of f iff the order of f does not divide n.
Русский
Для конечного β и цикла f поддержка f^n совпадает с поддержкой f тогда и только тогда, когда порядок f не делится на n.
LaTeX
$$$\\forall \\beta, f : \\mathrm{Perm}(\\beta),\\; \\mathrm{IsCycle}(f) \\Rightarrow \\forall n \\in \\mathbb{N},\\; \\mathrm{supp}(f^n) = \\mathrm{supp}(f) \\iff \\lnot (\\mathrm{orderOf}(f) \\mid n).$$$
Lean4
theorem support_pow_eq_iff (hf : IsCycle f) {n : ℕ} : support (f ^ n) = support f ↔ ¬orderOf f ∣ n :=
by
rw [orderOf_dvd_iff_pow_eq_one]
constructor
· intro h H
refine hf.ne_one ?_
rw [← support_eq_empty_iff, ← h, H, support_one]
· intro H
apply le_antisymm (support_pow_le _ n) _
intro x hx
contrapose! H
ext z
by_cases hz : f z = z
· rw [pow_apply_eq_self_of_apply_eq_self hz, one_apply]
· obtain ⟨k, rfl⟩ := hf.exists_pow_eq hz (mem_support.mp hx)
apply (f ^ k).injective
rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply]
simpa using H
