## Stream: maths

### Topic: dfinsupp vs finsupp

#### 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 α (λ _, β).

#### 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.

#### 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).

#### Kenny Lau (Oct 06 2019 at 21:22):

Yep. That's why I chose it.

Last updated: May 12 2021 at 07:17 UTC