English
The cardinality of the quotient of the normalizer by H.normalizer-subtype quotients is congruent modulo p to the cardinality of G/H.
Русский
Кардинальность нормализатора в квадрате по отношению к H имеет конгруэнтность по модулю p к кардинальности G/H.
LaTeX
$$card(normalizer H / comap (normalizer H).subtype H) ≡ card(G / H) [MOD p]$$
Lean4
/-- If `H` is a `p`-subgroup but not a Sylow `p`-subgroup of cardinality `p ^ n`,
then `p ^ (n + 1)` divides the cardinality of the normalizer of `H`. -/
theorem prime_pow_dvd_card_normalizer [Finite G] {p : ℕ} {n : ℕ} [_hp : Fact p.Prime] (hdvd : p ^ (n + 1) ∣ Nat.card G)
{H : Subgroup G} (hH : Nat.card H = p ^ n) : p ^ (n + 1) ∣ Nat.card (normalizer H) :=
Nat.modEq_zero_iff_dvd.1 ((card_normalizer_modEq_card hH).trans hdvd.modEq_zero_nat)
