Commit 2025-03-21 20:36 592a5a0b
View on Github →feat(Topology/Algebra/InfiniteSum/Order): positivity extension for infinite sums (#21557)
Add a positivity extension for tsum. This extension only attempts to prove nonnegativity goals, as proving positivity requires wrestling with convergence.