English
If relIndex P.normalizer ≠ 0, then p does not divide P.index.
Русский
Если relIndex(P.normalizer) ≠ 0, то p не делится на P.index.
LaTeX
$$$\\text{If } (P.\\mathrm{relIndex} \\; P.\\mathrm{normalizer}) \\neq 0,\\ \\ p \\nmid [G : P].$$$
Lean4
/-- A Sylow p-subgroup has index indivisible by `p`, assuming [N(P) : P] < ∞. -/
theorem not_dvd_index' [hp : Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) (hP : P.relIndex P.normalizer ≠ 0) :
¬p ∣ P.index := by
rw [← relIndex_mul_index le_normalizer, ← card_eq_index_normalizer]
haveI : (P.subtype le_normalizer).Normal := Subgroup.normal_in_normalizer
haveI : (P.subtype le_normalizer).FiniteIndex := ⟨hP⟩
replace hP := not_dvd_index_aux (P.subtype le_normalizer)
exact hp.1.not_dvd_mul hP (not_dvd_card_sylow p G)
