Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-04 22:36 d6a57f89

View on Github →

feat(data/finset/prod): When finset.product is nonempty (#10170) and two lemmas about how it interacts with the union.

Estimated changes

added theorem finset.nonempty.fst
added theorem finset.nonempty.snd
added theorem finset.product_union
added theorem finset.union_product