English
If G has a p-group with size at least p^n, there exists a subgroup of G of size p^n.
Русский
Если в G есть подгруппа p-порядка не меньше p^n, существует подгруппа G порядка p^n.
LaTeX
$$∃ H ≤ G, card H = p^n$$
Lean4
/-- A special case of **Sylow's first theorem**. If `G` is a `p`-group and `H` a subgroup of size at
least `k` then there is a subgroup of `H` of cardinality between `k / p` and `k`. -/
theorem exists_subgroup_le_card_le {k p : ℕ} (hp : p.Prime) (h : IsPGroup p G) {H : Subgroup G} (hk : k ≤ Nat.card H)
(hk₀ : k ≠ 0) : ∃ H' ≤ H, Nat.card H' ≤ k ∧ k < p * Nat.card H' :=
by
obtain ⟨m, hmk, hkm⟩ : ∃ s, p ^ s ≤ k ∧ k < p ^ (s + 1) :=
exists_nat_pow_near (Nat.one_le_iff_ne_zero.2 hk₀) hp.one_lt
obtain ⟨H', H'H, H'card⟩ := exists_subgroup_le_card_pow_prime_of_le_card hp h (hmk.trans hk)
refine ⟨H', H'H, ?_⟩
simpa only [pow_succ', H'card] using And.intro hmk hkm
