Commit 2025-04-10 06:47 1a43393f

feat: add Finset.prod_toList and rename existing Finset.prod_to_list (#23883) I was disappointed to find that (s : Finset α).toList.prod didn't simplify, so I added the simp lemma. There was already an existing simp lemma for (s.toList.map f).prod which was misnamed Finset.prod_to_list. This updated the latter to Finset.prod_map_toList and deprecates the old name.