mathlib3

3449510c - feat(algebra/big_operators): Alternative phrasing of prod-bij (#2709)

feat(algebra/big_operators): Alternative phrasing of prod-bij (#2709) Requested by @ChrisHughes24 in https://github.com/leanprover-community/mathlib/pull/2688/files#r426184248 A repaired version of #2708.