case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝² : MulAction G α
inst✝¹ : Fintype α
hpα : ¬p ∣ card α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
⊢ Nonempty ↑(fixedPoints G α)
p : ℕ
G : Type u_2
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝² : MulAction G α
inst✝¹ : Fintype α
hpα : ¬p ∣ card α
inst✝ : Finite ↑(fixedPoints G α)
⊢ Nonempty ↑(fixedPoints G α)
cases nonempty_fintype (fixedPoints G α)
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝² : MulAction G α
inst✝¹ : Fintype α
hpα : ¬p ∣ card α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
⊢ card ↑(fixedPoints G α) ≠ 0
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝² : MulAction G α
inst✝¹ : Fintype α
hpα : ¬p ∣ card α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
⊢ Nonempty ↑(fixedPoints G α)
rw [← card_pos_iff, pos_iff_ne_zero]
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
hpα : card ↑(fixedPoints G α) = 0
⊢ p ∣ card α
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝² : MulAction G α
inst✝¹ : Fintype α
hpα : ¬p ∣ card α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
⊢ card ↑(fixedPoints G α) ≠ 0
contrapose! hpα
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
hpα : card ↑(fixedPoints G α) = 0
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
hpα : card ↑(fixedPoints G α) = 0
⊢ p ∣ card α
rw [← Nat.modEq_zero_iff_dvd, ← hpα]
no goals
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
hpα : card ↑(fixedPoints G α) = 0
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]
exact hG.card_modEq_card_fixedPoints α