Commit 2024-07-23 13:03 cdc5e652
View on Github →chore(Finset): Rename noncommProd_map to map_noncommProd (#15048)
This matches the naming of map_multiset_prod
Moves:
- Multiset.noncommProd_map_aux -> Multiset.map_noncommProd_aux
- Multiset.noncommSum_map_aux -> Multiset.map_noncommSum_aux
- Multiset.noncommProd_map -> Multiset.map_noncommProd
- Multiset.noncommSum_map -> Multiset.map_noncommSum
- Finset.noncommProd_map -> Finset.map_noncommProd
- Finset.noncommSum_map -> Finset.map_noncommSum