English
If there exists a subgroup of cardinality p^n in a finite group G and p^n divides |G|, then there exists a subgroup of cardinality p^{n+1} containing the first subgroup.
Русский
Если в конечной группе G есть подгруппа кардинальности p^n и p^{n+1} делит |G|, то существует подгруппа кардинальности p^{n+1}, содержащая данную.
LaTeX
$$∃K: Subgroup G, card K = p^{n+1} ∧ H ≤ K$$
Lean4
/-- If `H` is a subgroup of `G` of cardinality `p ^ n`, then the cardinality of the
normalizer of `H` is congruent mod `p ^ (n + 1)` to the cardinality of `G`. -/
theorem card_normalizer_modEq_card [Finite G] {p : ℕ} {n : ℕ} [hp : Fact p.Prime] {H : Subgroup G}
(hH : Nat.card H = p ^ n) : Nat.card (normalizer H) ≡ Nat.card G [MOD p ^ (n + 1)] :=
by
have : H.subgroupOf (normalizer H) ≃ H := (subgroupOfEquivOfLe le_normalizer).toEquiv
rw [card_eq_card_quotient_mul_card_subgroup H, card_eq_card_quotient_mul_card_subgroup (H.subgroupOf (normalizer H)),
Nat.card_congr this, hH, pow_succ']
exact (card_quotient_normalizer_modEq_card_quotient hH).mul_right' _
