feat(algebra/big_operators/finprod): add a few lemmas (#7130)
* add `finprod_nonneg`, `finprod_cond_nonneg`, and `finprod_eq_zero`;
* use `α → Prop` instead of `set α` in
`finprod_mem_eq_prod_of_mem_iff`, rename to `finprod_cond_eq_prod_of_cond_iff`.
