Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-28 14:08 b71d38ce

View on Github →

feat(algebra/big_operators/basic): add lemmas about prod and sum of finset.erase (#8449) This adds:

  • finset.prod_erase_mul
  • finset.mul_prod_erase
  • finset.sum_erase_add
  • finset.add_sum_erase

Estimated changes

added theorem finset.mul_prod_erase
added theorem finset.prod_erase_mul