mathlib3

11bd2a08 - feat(big_operators/basic): sum of count over finset.filter equals countp (#15393)

feat(big_operators/basic): sum of count over finset.filter equals countp (#15393) The sum of `l.count x` over `x` in `l.to_finset.filter p` is equal to `l.countp p`. Also includes `prod_eq_one` instances for `list` and `multiset`