# mathlibdocumentation

group_theory.sylow

# 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 of G.
• All Sylow p-subgroups of G are conjugate to each other.
• Let nₚ be the number of Sylow p-subgroups of G, then nₚ divides the index of the Sylow p-subgroup, nₚ ≡ 1 [MOD p], and nₚ is equal to the index of the normalizer of the Sylow p-subgroup in G.

In this file, currently only the first of these results is proven.

## Main statements #

• exists_prime_order_of_dvd_card: For every prime p dividing the order of G there exists an element of order p in G. This is known as Cauchys theorem.
• exists_subgroup_card_pow_prime: A generalisation of the first of the Sylow theorems: For every prime power pⁿ dividing G, there exists a subgroup of G of order pⁿ.

## TODO #

• Prove the second and third of the Sylow theorems.
• Sylow theorems for infinite groups
theorem mul_action.mem_fixed_points_iff_card_orbit_eq_one {G : Type u} {α : Type v} [group G] [ α] {a : α} [fintype a)] :
= 1
theorem mul_action.card_modeq_card_fixed_points {G : Type u} {α : Type v} [group G] [ α] [fintype α] [fintype G] [fintype ] (p : ) {n : } [hp : fact (nat.prime p)] (h : = p ^ n) :
theorem quotient_group.card_preimage_mk {G : Type u} [group G] [fintype G] (s : subgroup G) (t : set ) :
def sylow.mk_vector_prod_eq_one {G : Type u} [group G] (n : ) (v : n) :
(n + 1)

Given a vector v of length n, make a vector of length n+1 whose product is 1, by consing the the inverse of the product of v.

Equations
theorem sylow.mk_vector_prod_eq_one_injective {G : Type u} [group G] (n : ) :
def sylow.vectors_prod_eq_one (G : Type u_1) [group G] (n : ) :
set (vector G n)

The type of vectors with terms from G, length n, and product equal to 1:G.

Equations
theorem sylow.mem_vectors_prod_eq_one {G : Type u} [group G] {n : } (v : n) :
theorem sylow.mem_vectors_prod_eq_one_iff {G : Type u} [group G] {n : } (v : (n + 1)) :
v (n + 1)
def sylow.rotate_vectors_prod_eq_one (G : Type u_1) [group G] (n : ) (m : multiplicative (zmod n)) (v : ) :

The rotation action of zmod n (viewed as multiplicative group) on vectors_prod_eq_one G n, where G` is a multiplicative group.

Equations
@[instance]
Equations
theorem sylow.one_mem_vectors_prod_eq_one {G : Type u} [group G] (n : ) :
theorem sylow.one_mem_fixed_points_rotate {G : Type u} [group G] (n : ) [fact (0 < n)] :
, _⟩
theorem sylow.exists_prime_order_of_dvd_card {G : Type u} [group G] [fintype G] (p : ) [hp : fact (nat.prime p)] (hdvd : p ) :
∃ (x : G), = p

Cauchy's theorem

Equations
theorem sylow.exists_subgroup_card_pow_prime {G : Type u} [group G] [fintype G] (p : ) {n : } [hp : fact (nat.prime p)] (hdvd : p ^ n ) :
∃ (H : subgroup G), = p ^ n

The first of the Sylow theorems.