Commit 2021-02-22 14:12 26e6d4cb

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