mathlib

60d14579 - chore(algebra/big_operators): drop some `decidable_eq` assumptions (#2332)

chore(algebra/big_operators): drop some `decidable_eq` assumptions (#2332) * chore(algebra/big_operators): drop some `decidable_eq` assumptions I wonder why `lint` didn't report them. * Drop unused arguments Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>