# Documentation

Mathlib.GroupTheory.Solvable

# Solvable Groups #

In this file we introduce the notion of a solvable group. We define a solvable group as one whose derived series is eventually trivial. This requires defining the commutator of two subgroups and the derived series of a group.

## Main definitions #

• derivedSeries G n : the nth term in the derived series of G, defined by iterating general_commutator starting with the top subgroup
• IsSolvable G : the group G is solvable
def derivedSeries (G : Type u_1) [] :

The derived series of the group G, obtained by starting from the subgroup ⊤ and repeatedly taking the commutator of the previous subgroup with itself for n times.

Equations
Instances For
@[simp]
theorem derivedSeries_zero (G : Type u_1) [] :
@[simp]
theorem derivedSeries_succ (G : Type u_1) [] (n : ) :
theorem derivedSeries_normal (G : Type u_1) [] (n : ) :
@[simp]
theorem derivedSeries_one (G : Type u_1) [] :
=
theorem map_derivedSeries_le_derivedSeries {G : Type u_1} {G' : Type u_2} [] [Group G'] (f : G →* G') (n : ) :
theorem derivedSeries_le_map_derivedSeries {G : Type u_1} {G' : Type u_2} [] [Group G'] {f : G →* G'} (hf : ) (n : ) :
theorem map_derivedSeries_eq {G : Type u_1} {G' : Type u_2} [] [Group G'] {f : G →* G'} (hf : ) (n : ) :
theorem isSolvable_def (G : Type u_1) [] :
n, =
class IsSolvable (G : Type u_1) [] :
• solvable : n, =

A group G is solvable if its derived series is eventually trivial.

A group G is solvable if its derived series is eventually trivial. We use this definition because it's the most convenient one to work with.

Instances
instance CommGroup.isSolvable {G : Type u_3} [] :
theorem isSolvable_of_comm {G : Type u_3} [hG : ] (h : ∀ (a b : G), a * b = b * a) :
theorem isSolvable_of_top_eq_bot (G : Type u_1) [] (h : ) :
instance isSolvable_of_subsingleton (G : Type u_1) [] [] :
theorem solvable_of_ker_le_range {G : Type u_1} [] {G' : Type u_3} {G'' : Type u_4} [Group G'] [Group G''] (f : G' →* G) (g : G →* G'') (hfg : ) [hG' : ] [hG'' : IsSolvable G''] :
theorem solvable_of_solvable_injective {G : Type u_1} {G' : Type u_2} [] [Group G'] {f : G →* G'} (hf : ) [] :
instance subgroup_solvable_of_solvable {G : Type u_1} [] (H : ) [] :
IsSolvable { x // x H }
theorem solvable_of_surjective {G : Type u_1} {G' : Type u_2} [] [Group G'] {f : G →* G'} (hf : ) [] :
instance solvable_quotient_of_solvable {G : Type u_1} [] (H : ) [] [] :
instance solvable_prod {G : Type u_1} [] {G' : Type u_3} [Group G'] [] [] :
IsSolvable (G × G')
theorem IsSimpleGroup.derivedSeries_succ {G : Type u_1} [] [] {n : } :
=
theorem IsSimpleGroup.comm_iff_isSolvable {G : Type u_1} [] [] :
(∀ (a b : G), a * b = b * a)
theorem not_solvable_of_mem_derivedSeries {G : Type u_1} [] {g : G} (h1 : g 1) (h2 : ∀ (n : ), g ) :
theorem Equiv.Perm.not_solvable (X : Type u_3) (hX : 5 ) :