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
this : { x // x ∈ subgroupOf H (normalizer H) } ≃ { x // x ∈ H }
⊢ Fintype.card { x // x ∈ normalizer H } ≡ Fintype.card G [MOD p ^ (n + 1)]
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 } ≡ Fintype.card G [MOD p ^ (n + 1)]
have : H.subgroupOf (normalizer H) ≃ H := (subgroupOfEquivOfLe le_normalizer).toEquiv
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
this : { x // x ∈ subgroupOf H (normalizer H) } ≃ { x // x ∈ H }
⊢ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) * p ^ n ≡ Fintype.card (G ⧸ H) * p ^ n [MOD
    p * p ^ n]
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
this : { x // x ∈ subgroupOf H (normalizer H) } ≃ { x // x ∈ H }
⊢ Fintype.card { x // x ∈ normalizer H } ≡ Fintype.card G [MOD p ^ (n + 1)]
rw [card_eq_card_quotient_mul_card_subgroup H,
  card_eq_card_quotient_mul_card_subgroup (H.subgroupOf (normalizer H)), Fintype.card_congr this,
  hH, pow_succ]
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
this : { x // x ∈ subgroupOf H (normalizer H) } ≃ { x // x ∈ H }
⊢ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) * p ^ n ≡ Fintype.card (G ⧸ H) * p ^ n [MOD
    p * p ^ n]
exact (card_quotient_normalizer_modEq_card_quotient hH).mul_right' _