Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.prod_filter_of_ne

Modification history

2020-07-12 03:42

src/algebra/big_operators.lean

feat(data/set/finite): add a version of `prod_preimage` for `inj_on` (#3342) …

Added finset.prod_filter_of_ne View on Github →