mathlib3

d23fd6f7 - refactor(group_theory/solvable): Golf and move `solvable_of_ker_le_range` (#13254)

refactor(group_theory/solvable): Golf and move `solvable_of_ker_le_range` (#13254) This PR moves `solvable_of_ker_le_range` to earlier in the file so that it can be used to golf the proofs of `solvable_of_solvable_injective` and `solvable_of_surjective`.