mathlib3

3dd12573 - feat(group_theory/solvable): Commutative groups are solvable (#6625)

feat(group_theory/solvable): Commutative groups are solvable (#6625) In practice, `is_solvable_of_comm` is hard to use, since you often aren't working with a `comm_group`. Instead, it is much nicer to be able to write: `apply is_solvable_of_comm'` `intros g h`