Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-04 15:29 69189d44

View on Github →

split(data/finset/prod): split off data.finset.basic (#10142) Killing the giants. This moves finset.product, finset.diag, finset.off_diag to their own file, the theme being "finsets on α × β". The copyright header now credits:

  • Johannes Hölzl for ba95269a65a77c8ab5eae075f842fdad0c0a7aaf
  • Mario Carneiro
  • Oliver Nash for #4502

Estimated changes

deleted theorem finset.card_product
deleted def finset.diag
deleted theorem finset.diag_card
deleted theorem finset.diag_empty
deleted theorem finset.empty_product
deleted theorem finset.filter_product
deleted theorem finset.mem_diag
deleted theorem finset.mem_off_diag
deleted theorem finset.mem_product
deleted def finset.off_diag
deleted theorem finset.off_diag_card
deleted theorem finset.off_diag_empty
deleted theorem finset.product_bUnion
deleted theorem finset.product_empty
deleted theorem finset.product_eq_bUnion
deleted theorem finset.product_val
deleted theorem finset.subset_product
added theorem finset.card_product
added def finset.diag
added theorem finset.diag_card
added theorem finset.diag_empty
added theorem finset.empty_product
added theorem finset.filter_product
added theorem finset.mem_diag
added theorem finset.mem_off_diag
added theorem finset.mem_product
added def finset.off_diag
added theorem finset.off_diag_card
added theorem finset.off_diag_empty
added theorem finset.product_bUnion
added theorem finset.product_empty
added theorem finset.product_val
added theorem finset.subset_product