mathlib3

2a49f4e5 - feat(algebra/lie/direct_sum): direct sums of Lie modules (#5063)

feat(algebra/lie/direct_sum): direct sums of Lie modules (#5063) There are three things happening here: 1. introduction of definitions of direct sums for Lie modules, 2. introduction of definitions of morphisms, equivs for Lie modules, 3. splitting out extant definition of direct sums for Lie algebras into a new file.