prod): When `finset.product` is nonempty (#10170)

Commit

4 years ago

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

Author

YaelDillies

Parents