English
If σ^{p^n} = 1 for a prime p, then the cardinality of the complement of σ's support is congruent to |α| modulo p.
Русский
Если σ^{p^n} = 1 для простого p, то |σ.support^c| ≡ |α| (mod p).
LaTeX
$$$$ σ^{p^{n}} = 1 \implies \#(σ.\mathrm{support}^{c}) \equiv |\alpha| \pmod p. $$$$
Lean4
theorem card_compl_support_modEq [DecidableEq α] {p n : ℕ} [hp : Fact p.Prime] {σ : Perm α} (hσ : σ ^ p ^ n = 1) :
σ.supportᶜ.card ≡ Fintype.card α [MOD p] :=
by
rw [Nat.modEq_iff_dvd', ← Finset.card_compl, compl_compl, ← sum_cycleType]
· refine Multiset.dvd_sum fun k hk => ?_
obtain ⟨m, -, hm⟩ := (Nat.dvd_prime_pow hp.out).mp (orderOf_dvd_of_pow_eq_one hσ)
obtain ⟨l, -, rfl⟩ := (Nat.dvd_prime_pow hp.out).mp ((congr_arg _ hm).mp (dvd_of_mem_cycleType hk))
exact dvd_pow_self _ fun h => (one_lt_of_mem_cycleType hk).ne <| by rw [h, pow_zero]
· exact Finset.card_le_univ _
