English
If H is a p-subgroup of G with card(H) = p^n, then p divides the card of the quotient of the normalizer by H-normalizer-subtype comap.
Русский
Если H — p-подгруппа группы G и |H| = p^n, тогда p делит кардинал квадрата нормализатора по H.
LaTeX
$$p ∣ card(normalizer H / comap (normalizer H).subtype H)$$
Lean4
/-- If `H` is a `p`-subgroup but not a Sylow `p`-subgroup, then `p` divides the
index of `H` inside its normalizer. -/
theorem prime_dvd_card_quotient_normalizer [Finite G] {p : ℕ} {n : ℕ} [Fact p.Prime] (hdvd : p ^ (n + 1) ∣ Nat.card G)
{H : Subgroup G} (hH : Nat.card H = p ^ n) :
p ∣ Nat.card (normalizer H ⧸ Subgroup.comap ((normalizer H).subtype : normalizer H →* G) H) :=
let ⟨s, hs⟩ := exists_eq_mul_left_of_dvd hdvd
have hcard : Nat.card (G ⧸ H) = s * p :=
(mul_left_inj' (show Nat.card H ≠ 0 from Nat.card_pos.ne')).1
(by rw [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p])
have hm : s * p % p = Nat.card (normalizer H ⧸ Subgroup.comap ((normalizer H).subtype : normalizer H →* G) H) % p :=
hcard ▸ (card_quotient_normalizer_modEq_card_quotient hH).symm
Nat.dvd_of_mod_eq_zero (by rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm)
