direct sum vs dfinsupp

Stream: maths

[Johan Commelin]

Do we have ideas about what the API boundary between direct_sum and dfinsupp should look like? Do we want both, or should we just get rid of one of them? See also https://github.com/leanprover-community/mathlib/pull/5204#pullrequestreview-549446922

[Eric Wieser]

docs#dfinsupp, docs#direct_sum

[Eric Wieser]

Perhaps this brings up a shelved argument about docs#monoid_algebra; that both monoid_algebra and direct_sum should not implement has_coe_to_fun, but instead have some other named accesor