feat(algebra/big_operators/basic): add finset.prod_to_list (#10842)

Co-authored-by: jlh <48520973+Jlh18@users.noreply.github.com>

src/algebra/big_operators/basic.lean

@@ -251,6 +251,14 @@ begin
   rw [← prod_union (filter_inter_filter_neg_eq p s).le, filter_union_filter_neg_eq]
 end
 
+section to_list
+
+@[simp, to_additive]
+lemma prod_to_list (s : finset α) (f : α → β) : (s.to_list.map f).prod = s.prod f :=
+by rw [finset.prod, ← multiset.coe_prod, ← multiset.coe_map, finset.coe_to_list]
+
+end to_list
+
 end comm_monoid
 
 end finset