G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
⊢ Fintype.card ↑(MulAction.fixedPoints { x // x ∈ H } (G ⧸ H)) ≡ Fintype.card (G ⧸ H) [MOD p]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
⊢ Fintype.card ({ x // x ∈ normalizer H } ⧸ Subgroup.comap (Subgroup.subtype (normalizer H)) H) ≡
    Fintype.card (G ⧸ H) [MOD p]
rw [← Fintype.card_congr (fixedPointsMulLeftCosetsEquivQuotient H)]
no goals
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
⊢ Fintype.card ↑(MulAction.fixedPoints { x // x ∈ H } (G ⧸ H)) ≡ Fintype.card (G ⧸ H) [MOD p]
exact ((IsPGroup.of_card hH).card_modEq_card_fixedPoints _).symm