no goals
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ ∃ a, ↑σ a = a
classical
  contrapose! hα
  simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
  exact Nat.modEq_zero_iff_dvd.1 ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp
    (card_compl_support_modEq hσ).symm)
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : ∀ (a : α), ↑σ a ≠ a
⊢ p ∣ Fintype.card α
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ ∃ a, ↑σ a = a
contrapose! hα
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : support σ = Finset.univ
⊢ p ∣ Fintype.card α
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : ∀ (a : α), ↑σ a ≠ a
⊢ p ∣ Fintype.card α
simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
no goals
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : support σ = Finset.univ
⊢ p ∣ Fintype.card α
exact Nat.modEq_zero_iff_dvd.1 ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp
  (card_compl_support_modEq hσ).symm)