Commit 2020-11-23 22:04 2a49f4e5
View on Github →feat(algebra/lie/direct_sum): direct sums of Lie modules (#5063) There are three things happening here:
- introduction of definitions of direct sums for Lie modules,
- introduction of definitions of morphisms, equivs for Lie modules,
- splitting out extant definition of direct sums for Lie algebras into a new file.