mathlib

5c433d03 - feat(algebra/big_operators/basic): `prod_list_count` and `prod_list_count_of_subset` (#13370)

feat(algebra/big_operators/basic): `prod_list_count` and `prod_list_count_of_subset` (#13370) Add `prod_list_count (l : list α) : l.prod = ∏ x in l.to_finset, (x ^ (l.count x))` and `prod_list_count_of_subset (l : list α) (s : finset α) (hs : l.to_finset ⊆ s) : l.prod = ∏ x in s, x ^ (l.count x)` as counterparts of `prod_multiset_count` and `prod_multiset_count_of_subset` (whose proofs are then golfed using the new lemmas).