Zulip Chat Archive

Stream: maths

Topic: direct sum vs dfinsupp


view this post on Zulip Johan Commelin (Dec 10 2020 at 18:21):

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

view this post on Zulip Eric Wieser (Dec 10 2020 at 18:28):

docs#dfinsupp, docs#direct_sum

view this post on Zulip Eric Wieser (Dec 10 2020 at 18:29):

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


Last updated: May 18 2021 at 08:14 UTC