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 #
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
G is solvable if its derived series is eventually trivial. We use this definition
because it's the most convenient one to work with.