Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-31 23:00 932e9548

View on Github →

feat(data/finset): some simple finset lemmas (#10079)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.diag_empty

added theorem finset.off_diag_empty

added theorem finset.product_subset_product

added theorem finset.product_subset_product_left

added theorem finset.product_subset_product_right