not_dvd_index — Mathlib

English

Let p be a prime. If P is a Sylow p-subgroup of a finite group G and P has finite index, then p does not divide the index [G : P].

Русский

Пусть p — простое. Если P являетсяSylow p-подгруппой конечной группы G и индекс [G : P] конечен, то p не делит этот индекс.

LaTeX

$$$p \\nmid [G : P]$$$

Lean4

/-- A Sylow p-subgroup has index indivisible by `p`. -/
theorem not_dvd_index [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) [P.FiniteIndex] : ¬p ∣ P.index :=
  P.not_dvd_index' Nat.card_pos.ne'

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