mathlib

dd72ebc0 - feat(data/list/big_operators): When `list.sum` is strictly positive (#10282)