Develop the List.sum, List.prod and related APIs #1465
Description
Mathlib's BigOperators library is well-developed, sophisticated and works extremely well. There is however a need for a less sophisticated intermediate library built directly on Std's basic classes for associativity, commutativity, identities. Just downstreaming Mathlib's API is not possible since many features don't fit in Batteries' focus on programming and formal verification.
We need a plan for this. This plan should balance low-level and high-level features, enhancing Std's basic API in a manner compatible with Mathlib's API. This plan should strengthen both Std and Mathlib, while staying within the scope of Batteries.