Sylow theorems #
The Sylow theorems are the following results for every finite group
G and every prime number
- There exists a Sylow
- All Sylow
Gare conjugate to each other.
nₚbe the number of Sylow
nₚdivides the index of the Sylow
nₚ ≡ 1 [MOD p], and
nₚis equal to the index of the normalizer of the Sylow
In this file, currently only the first of these results is proven.
Main statements #
exists_prime_order_of_dvd_card: For every prime
pdividing the order of
Gthere exists an element of order
G. This is known as Cauchy`s theorem.
exists_subgroup_card_pow_prime: A generalisation of the first of the Sylow theorems: For every prime power
G, there exists a subgroup of
- Prove the second and third of the Sylow theorems.
- Sylow theorems for infinite groups
The rotation action of
zmod n (viewed as multiplicative group) on
vectors_prod_eq_one G n, where
G is a multiplicative group.