feat(data/list/basic): add `list.prod_eq_zero(_iff)` (#6504)
API changes:
* add `list.prod_eq_zero`, `list.prod_eq_zero_iff`, ;
* lemmas `list.prod_ne_zero`, `multiset.prod_ne_zero`, `polynomial.root_list_prod`, `polynomial.roots_multiset_prod`, `polynomial.nat_degree_multiset_prod`, now assume `0 ∉ L` (or `0 ∉ m`/`0 ∉ s`) instead of `∀ x ∈ L, x ≠ 0`
