exists_subgroup_card_pow_prime_of_le_card

English

If G has a normal Sylow p-subgroup, then it is the only Sylow p-subgroup of G.

Русский

Если в G существует нормальная Sylow p-подгруппа, то она единственна среди Sylow p-subгрупп.

LaTeX

$$Unique (Sylow p G)$$

Lean4

/-- A special case of **Sylow's first theorem**. If `G` is a `p`-group of size at least `p ^ n`
then there is a subgroup of cardinality `p ^ n`. -/
theorem exists_subgroup_card_pow_prime_of_le_card {n p : ℕ} (hp : p.Prime) (h : IsPGroup p G)
    (hn : p ^ n ≤ Nat.card G) : ∃ H : Subgroup G, Nat.card H = p ^ n :=
  by
  have : Fact p.Prime := ⟨hp⟩
  have : Finite G := Nat.finite_of_card_ne_zero <| by linarith [Nat.one_le_pow n p hp.pos]
  obtain ⟨m, hm⟩ := h.exists_card_eq
  refine exists_subgroup_card_pow_prime _ ?_
  rw [hm] at hn ⊢
  exact pow_dvd_pow _ <| (Nat.pow_le_pow_iff_right hp.one_lt).1 hn

Похожие утверждения