Commit 2020-05-02 15:22 a99f9b55
View on Github →refactor(algebra/big_operators): introduce notation for finset.prod and finset.sum (#2582) I have not gone through all of mathlib to use this notation everywhere. I think we can maybe transition naturally.