index — Mathlib

English

If G is a p-group, then every finite-index subgroup H of G has index p^n for some n.

Русский

Если G — p-группа, то любой подгрупповой индекс H имеет вид p^n для некоторого n.

LaTeX

$$$\IsPGroup(p,G) \rightarrow \forall (H : Subgroup G)[H.FiniteIndex], \exists n, H.index = p^n$$$

Lean4

theorem index (H : Subgroup G) [H.FiniteIndex] : ∃ n : ℕ, H.index = p ^ n :=
  by
  obtain ⟨n, hn⟩ := iff_card.mp (hG.to_quotient H.normalCore)
  obtain ⟨k, _, hk2⟩ :=
    (Nat.dvd_prime_pow hp.out).mp
      ((congr_arg _ (H.normalCore.index_eq_card.trans hn)).mp (Subgroup.index_dvd_of_le H.normalCore_le))
  exact ⟨k, hk2⟩

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