English
A p-subgroup P of G whose index [G : P] is not divisible by p sits inside a Sylow p-subgroup of G; more precisely, there exists a Sylow p-subgroup of G whose underlying subgroup equals P.
Русский
П-подгруппа P группы G с индексом, не делимым на p, содержится в Силовой подпгруппе p; точнее, найдётся Силова p-подгруппа, чья основанная подгруппа равна P.
LaTeX
$$$\\text{IsPGroup}(p, P) \\land \\neg p \\mid P.index \\Rightarrow \\exists Q : Sylow_p(G), Q.toSubgroup = P$$$
Lean4
/-- A `p`-subgroup with index indivisible by `p` is a Sylow subgroup. -/
def _root_.IsPGroup.toSylow [Fact p.Prime] {P : Subgroup G} (hP1 : IsPGroup p P) (hP2 : ¬p ∣ P.index) : Sylow p G :=
{ P with
isPGroup' := hP1
is_maximal' := by
intro Q hQ hPQ
have : P.FiniteIndex := ⟨fun h ↦ hP2 (h ▸ (dvd_zero p))⟩
obtain ⟨k, hk⟩ := (hQ.to_quotient (P.normalCore.subgroupOf Q)).exists_card_eq
have h := hk ▸ Nat.Prime.coprime_pow_of_not_dvd (m := k) Fact.out hP2
exact
le_antisymm
(Subgroup.relIndex_eq_one.mp
(Nat.eq_one_of_dvd_coprimes h (Subgroup.relIndex_dvd_index_of_le hPQ)
(Subgroup.relIndex_dvd_of_le_left Q P.normalCore_le)))
hPQ }
