mathlib documentation

group_theory.sylow

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 (nat.prime p)] :

def sylow.mk_vector_prod_eq_one {G : Type u} [group G] (n : ) :
vector G nvector 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.

Equations
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 : 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.

Equations
theorem sylow.exists_prime_order_of_dvd_card {G : Type u} [group G] [fintype G] (p : ) [hp : fact (nat.prime p)] :
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 (nat.prime p)] :
p ^ n fintype.card G(∃ (H : subgroup G), fintype.card H = p ^ n)