Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-24 11:15 8187142b

View on Github →

feat(data/finset/pointwise): s • t is the union of the a • t (#14696) and a few other results leading to it. Also tag set.coe_bUnion with norm_cast and rename finset.image_mul_prod/finset.add_image_prod to finset.image_mul_product/finset.image_add_product

Estimated changes