Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-17 23:26 043d046a

View on Github →

feat(algebra/lie/basic): define the module and lie_module structures on morphisms of Lie modules (#7225) Also sundry simp lemmas

Estimated changes

added theorem bracket_apply
added theorem lie_hom.coe_linear_mk
added theorem lie_hom.coe_zero
added theorem lie_hom.map_neg
added theorem lie_hom.map_sub
added theorem lie_hom.mk_coe
added theorem lie_hom.zero_apply
added theorem lie_module_hom.coe_add
added theorem lie_module_hom.coe_neg
added theorem lie_module_hom.coe_sub
added theorem lie_module_hom.map_add
added theorem lie_module_hom.map_neg
added theorem lie_module_hom.map_sub
added theorem lie_module_hom.mk_coe
added theorem lie_nsmul
added theorem lie_sub
added theorem nsmul_lie
added theorem sub_lie