mathlib3

407615e0 - feat(algebra/lie/solvable): images of solvable Lie algebras are solvable (#6413)

feat(algebra/lie/solvable): images of solvable Lie algebras are solvable (#6413) Summary of changes: New definition: - `lie_hom.range_restrict` New lemmas: - `lie_ideal.derived_series_map_eq` - `function.surjective.lie_algebra_is_solvable` - `lie_algebra.solvable_iff_equiv_solvable` - `lie_hom.is_solvable_range` - `lie_hom.mem_range_self` - `lie_hom.range_restrict_apply` - `lie_hom.surjective_range_restrict` Renamed lemmas: - `lie_algebra.is_solvable_of_injective` → `function.injective.lie_algebra_is_solvable` - `lie_ideal.derived_series_map_le_derived_series` → `lie_ideal.derived_series_map_le`