Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.mul_prod_erase

Modification history

2021-07-28 14:08
src/algebra/big_operators/basic.lean
feat(algebra/big_operators/basic): add lemmas about prod and sum of finset.erase (#8449) …
Added finset.mul_prod_eraseView on Github →