mathlib

f9c787da - refactor(algebra/big_operators, *): specialize `finset.prod_bij` to `fintype.prod_equiv` (#7109)

refactor(algebra/big_operators, *): specialize `finset.prod_bij` to `fintype.prod_equiv` (#7109) Often we want to apply `finset.prod_bij` to the case where the product is taken over `finset.univ` and the bijection is already a bundled `equiv`. This PR adds `fintype.prod_equiv` as a specialization for exactly these cases, filling in most of the arguments already. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>