Commit 2022-03-08 15:58 4ad5c5a3

View on Github →

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

Estimated changes

Modified src/data/finset/noncomm_prod.lean

added theorem finset.noncomm_prod_commute

added theorem multiset.noncomm_prod_commute

Modified src/data/list/prod_monoid.lean

added theorem list.prod_commute