Commit 2021-06-02 04:56 6b2c7a75

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.