mathlib3

92f6eb6b - chore(algebra/big_operators/fin): golf finset.prod_range (#13535)