Commit 2022-04-08 21:51 485d6484
View on Github →feat(algebra/big_operators): some big operator lemmas (#13066)
Note that prod_coe_sort is essentially prod_finset_coe restated with the relatively new finset.has_coe_to_sort. I can also place prod_finset_coe with prod_coe_sort if we prefer.