mathlib documentation


Sylow theorems #

The Sylow theorems are the following results for every finite group G and every prime number p.

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

Main statements #


theorem mul_action.card_modeq_card_fixed_points {G : Type u} {α : Type v} [group G] [mul_action G α] [fintype α] [fintype G] [fintype (mul_action.fixed_points G α)] (p : ) {n : } [hp : fact ( p)] (h : fintype.card G = p ^ n) :
def sylow.mk_vector_prod_eq_one {G : Type u} [group G] (n : ) (v : vector G n) :
vector G (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.

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.

theorem sylow.mem_vectors_prod_eq_one {G : Type u} [group G] {n : } (v : vector G n) :

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

theorem sylow.exists_prime_order_of_dvd_card {G : Type u} [group G] [fintype G] (p : ) [hp : fact ( p)] (hdvd : p fintype.card G) :
∃ (x : G), order_of x = p

Cauchy's theorem

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

The first of the Sylow theorems