mathlib3

d5563aea - feat(group_theory/solvable): Solvability preserved by short exact sequences (#6632)

feat(group_theory/solvable): Solvability preserved by short exact sequences (#6632) Proves that if 0 -> A -> B -> C -> 0 is a short exact sequence of groups, and if A and C are both solvable, then so is B.