Commit 2021-02-26 20:32 407615e0

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