Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-11 19:18 5856c0c4

View on Github →

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

Estimated changes