mathlib

6b2c7a75 - feat(data/finset/noncomm_prod): finset products over monoid (#7567)

feat(data/finset/noncomm_prod): finset products over monoid (#7567) The regular `finset.prod` and `multiset.prod` require `[comm_monoid α]`. Often, there are collections `s : finset α` where `[monoid α]` and we know, in a dependent fashion, that for all the terms `∀ (x ∈ s) (y ∈ s), commute x y`. This allows to still have a well-defined product over `s`.