Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-26 13:34 5ac79a63

View on Github →

feat(algebra/lie/tensor_product): prove lie_submodule.lie_ideal_oper_eq_tensor_map_range (#7313) The lemma coe_lift_lie_eq_lift_coe also introduced here is an unrelated change but is a stronger form of lift_lie_apply that is worth having. See also this Zulip remark concerning the proposed library note.

Estimated changes

added theorem lie_hom.coe_comp
modified theorem lie_hom.comp_apply
deleted theorem lie_hom.comp_coe
modified theorem lie_module_hom.comp_apply
deleted theorem lie_module_hom.comp_coe
added theorem lie_module_hom.map_top
added theorem lie_submodule.mem_map