Zulip Chat Archive

Stream: maths

Topic: dfinsupp vs finsupp


view this post on Zulip Yury G. Kudryashov (Oct 06 2019 at 16:47):

Hi, I see that dfinsupp is implemented using multiset, pre_support, and quotient while finsupp is implemented using finset and support. Is there any particular reason for this difference?
I mean, before looking into the sources I expected finsupp α β = dfinsupp α (λ _, β).

view this post on Zulip Chris Hughes (Oct 06 2019 at 17:46):

No good reason really. I think they were just written at different times by different people with different tastes.

view this post on Zulip Yury G. Kudryashov (Oct 06 2019 at 19:55):

As far as I understand, dfinsupp works without some decidable_eq assumptions while finsupp doesn't (or creates noncomputable defs).

view this post on Zulip Kenny Lau (Oct 06 2019 at 21:22):

Yep. That's why I chose it.


Last updated: May 12 2021 at 07:17 UTC