noncomm_prod): add noncomm_prod_commute (#12521)

Commit

4 years ago

feat(data/finset/noncomm_prod): add noncomm_prod_commute (#12521) adding `list.prod_commute`, `multiset.noncomm_prod_commute` and `finset.noncomm_prod_commute`.

Author

nomeata

Parents

fac5ffed

mathlib3 4ad5c5a3 - feat(data/finset/noncomm_prod): add noncomm_prod_commute (#12521)

mathlib3
4ad5c5a3 - feat(data/finset/noncomm_prod): add noncomm_prod_commute (#12521)