noncomm_prod): add noncomm_prod_mul_distrib (#12524)

Commit

3 years ago

feat(data/finset/noncomm_prod): add noncomm_prod_mul_distrib (#12524) The non-commutative version of `finset.sum_union`.

Author

nomeata

Parents