direct_sum vs dfinsup

Stream: general

[Antoine Labelle]

What's the difference between docs#direct_sum and docs#dfinsupp? They both have a module structure when the factors themselves have a module structure, so I'm not sure which one I should use to talk about direct sums in linear algebra.

[Eric Wieser]

Right now, direct_sum is to add_monoid_algebra as dfinsupp is to finsupp