Commit 2020-11-23 22:04 2a49f4e5

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.