card_coprime_index — Mathlib

English

For a Sylow p-subgroup P in a finite group G, the order of P and the index [G:P] are relatively prime.

Русский

Для Sylow p-подгруппы P в конечной группе G порядок P и индекс [G:P] взаимно просты.

LaTeX

$$(|P|, [G:P]) = 1$$

Lean4

/-- Sylow subgroups are Hall subgroups. -/
theorem card_coprime_index [Finite G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G) : (Nat.card P).Coprime P.index :=
  let ⟨_n, hn⟩ := IsPGroup.iff_card.mp P.2
  hn.symm ▸ (hp.1.coprime_pow_of_not_dvd P.not_dvd_index).symm

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