mathlib3

26e6d4cb - feat(algebra/lie/{subalgebra,submodule}): grab bag of new lemmas (#6342)

feat(algebra/lie/{subalgebra,submodule}): grab bag of new lemmas (#6342) I'm splitting these off from other work to simplify subsequent reviews. Cosmetic changes aside, the following summarises what I am proposing: New definitions: - `lie_subalgebra.of_le` Definition tweaks: - `lie_hom.range` [use coercion instead of `lie_hom.to_linear_map`] - `lie_ideal.map` [factor through `submodule.map` to avoid dropping all the way down to `set.image`] New lemmas: - `lie_ideal.coe_to_lie_subalgebra_to_submodule` - `lie_ideal.incl_range` - `lie_hom.ideal_range_eq_lie_span_range` - `lie_hom.is_ideal_morphism_iff` - `lie_subalgebra.mem_range` - `lie_subalgebra.mem_map` - `lie_subalgebra.mem_of_le` - `lie_subalgebra.of_le_eq_comap_incl` - `lie_subalgebra.exists_lie_ideal_coe_eq_iff` - `lie_subalgebra.exists_nested_lie_ideal_coe_eq_iff` - `submodule.exists_lie_submodule_coe_eq_iff` - `lie_submodule.coe_lie_span_submodule_eq_iff` Deleted lemma: - `lie_hom.range_bracket` New simp attributes: - `lie_subalgebra.mem_top` - `lie_submodule.mem_top`