mathlib

c1600832 - feat(algebra/big_operators): `norm_num` plugin for list/multiset/finset prod/sum (#13005)

feat(algebra/big_operators): `norm_num` plugin for list/multiset/finset prod/sum (#13005) This PR provides a plugin for the `norm_num` tactic that can evaluate finite sums and products, over lists, multisets and finsets. `simp` could already handle some of these operations, but `norm_num` is overall much more suited to dealing with larger numerical operations such as arising from large sums. I implemented the tactic as a `norm_num` plugin since it's intended to deal with numbers. I'm happy to make it its own tactic (`norm_bigop`?) if you feel this is outside of the `norm_num` scope. Similarly, I could also make a separate tactic for the parts that rewrite a list/multiset/finset into a sequence of `list.cons`es.