pow_dvd_card_of_pow_dvd_card — Mathlib

English

The cardinality of a Sylow p-subgroup equals p^n where n is the exponent of p in |G|.

Русский

Кардинальность Sylow p-подгруппы равна p^n, где n — показатель степени p в |G|.

LaTeX

$$card P = p^{Nat.factorization |G| p}$$

Lean4

theorem pow_dvd_card_of_pow_dvd_card [Finite G] {p n : ℕ} [hp : Fact p.Prime] (P : Sylow p G)
    (hdvd : p ^ n ∣ Nat.card G) : p ^ n ∣ Nat.card P :=
  by
  rw [← index_mul_card P.1] at hdvd
  exact (hp.1.coprime_pow_of_not_dvd P.not_dvd_index).symm.dvd_of_dvd_mul_left hdvd

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