dvd_card_of_dvd_card — Mathlib

English

If p is prime and G is finite, then for any n with p^n | |G| there exists a subgroup of order p^n.

Русский

Пусть p — простое, G конечна. При любом n с p^n | |G| существует подгруппа порядка p^n.

LaTeX

$$∃ H: Subgroup G, card H = p^n$$

Lean4

theorem dvd_card_of_dvd_card [Finite G] {p : ℕ} [Fact p.Prime] (P : Sylow p G) (hdvd : p ∣ Nat.card G) :
    p ∣ Nat.card P := by
  rw [← pow_one p] at hdvd
  have key := P.pow_dvd_card_of_pow_dvd_card hdvd
  rwa [pow_one] at key

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