Commit 2019-04-14 15:16 a1b7dcdf

fix(algebra/big_operators): change variables in finset.prod_map to remove spurious [comm_monoid β] (#934) The old version involved maps α → β → γ and an instance [comm_monoid γ], but there was also a section variable [comm_monoid β]. In applications of this lemma it is not necessary, and not usually true, that β is a monoid. Change the statement to involve maps α → γ → β so that we already have a monoid structure on the last variable and we do not make spurious assumptions about the second one.