Sylow theorems #
The Sylow theorems are the following results for every finite group G
and every prime number p
.
- There exists a Sylow
p
-subgroup ofG
. - All Sylow
p
-subgroups ofG
are conjugate to each other. - Let
nₚ
be the number of Sylowp
-subgroups ofG
, thennₚ
divides the index of the Sylowp
-subgroup,nₚ ≡ 1 [MOD p]
, andnₚ
is equal to the index of the normalizer of the Sylowp
-subgroup inG
.
Main definitions #
Sylow p G
: The type of Sylowp
-subgroups ofG
.
Main statements #
exists_subgroup_card_pow_prime
: A generalization of Sylow's first theorem: For every prime powerpⁿ
dividing the cardinality ofG
, there exists a subgroup ofG
of orderpⁿ
.IsPGroup.exists_le_sylow
: A generalization of Sylow's first theorem: Everyp
-subgroup is contained in a Sylowp
-subgroup.Sylow.card_eq_multiplicity
: The cardinality of a Sylow subgroup isp ^ n
wheren
is the multiplicity ofp
in the group order.sylow_conjugate
: A generalization of Sylow's second theorem: If the number of Sylowp
-subgroups is finite, then all Sylowp
-subgroups are conjugate.card_sylow_modEq_one
: A generalization of Sylow's third theorem: If the number of Sylowp
-subgroups is finite, then it is congruent to1
modulop
.
A Sylow p
-subgroup is a maximal p
-subgroup.
Instances For
The preimage of a Sylow subgroup under a p-group-kernel homomorphism is a Sylow subgroup.
Instances For
The preimage of a Sylow subgroup under an injective homomorphism is a Sylow subgroup.
Instances For
Subgroup.pointwiseMulAction
preserves Sylow subgroups.
A generalization of Sylow's second theorem.
If the number of Sylow p
-subgroups is finite, then all Sylow p
-subgroups are conjugate.
Frattini's Argument: If N
is a normal subgroup of G
, and if P
is a Sylow p
-subgroup
of N
, then N_G(P) ⊔ N = G
.
Frattini's Argument: If N
is a normal subgroup of G
, and if P
is a Sylow p
-subgroup
of N
, then N_G(P) ⊔ N = G
.
The fixed points of the action of H
on its cosets correspond to normalizer H / H
.
Instances For
If H
is a p
-subgroup of G
, then the index of H
inside its normalizer is congruent
mod p
to the index of H
.
If H
is a subgroup of G
of cardinality p ^ n
, then the cardinality of the
normalizer of H
is congruent mod p ^ (n + 1)
to the cardinality of G
.
If H
is a p
-subgroup but not a Sylow p
-subgroup, then p
divides the
index of H
inside its normalizer.
If H
is a p
-subgroup but not a Sylow p
-subgroup of cardinality p ^ n
,
then p ^ (n + 1)
divides the cardinality of the normalizer of H
.
If H
is a subgroup of G
of cardinality p ^ n
,
then H
is contained in a subgroup of cardinality p ^ (n + 1)
if p ^ (n + 1)
divides the cardinality of G
If H
is a subgroup of G
of cardinality p ^ n
,
then H
is contained in a subgroup of cardinality p ^ m
if n ≤ m
and p ^ m
divides the cardinality of G
A generalisation of Sylow's first theorem. If p ^ n
divides
the cardinality of G
, then there is a subgroup of cardinality p ^ n
Sylow subgroups are Hall subgroups.
The cardinality of a Sylow subgroup is p ^ n
where n
is the multiplicity of p
in the group order.
A subgroup with cardinality p ^ n
is a Sylow subgroup
where n
is the multiplicity of p
in the group order.
Instances For
If all its Sylow subgroups are normal, then a finite group is isomorphic to the direct product of these Sylow subgroups.