mathlib3

131c39a4 - chore(algebra/big_operators): reorder the definitions in `norm_num` extension (#15840)

chore(algebra/big_operators): reorder the definitions in `norm_num` extension (#15840) This prepares for PR #15538, where `eval_finset` calls `eval_multiset`, which calls `eval_list`. By reordering in a separate PR, we get a cleaner diff.