Zulip Chat Archive
Stream: general
Topic: sum_equiv
Patrick Massot (Aug 09 2020 at 13:38):
Is there any reason why docs#finset.sum_equiv is in finset/card.lean instead of near the other bigops lemmas?
Yury G. Kudryashov (Aug 09 2020 at 17:34):
It needs fintype
Yury G. Kudryashov (Aug 09 2020 at 17:34):
And algebra/big_operators doesn't import fintype
Patrick Massot (Aug 09 2020 at 18:41):
We probably at least need a note in the bigop module docstring.
Last updated: Dec 20 2023 at 11:08 UTC