Def Mathlib.Meta.Positivity.evalTsum

Modification history

2025-11-19 06:07
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
chore: move Mathlib to the module system (#31786) …
Deleted Mathlib.Meta.Positivity.evalTsumView on Github →
2025-03-21 20:36
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
feat(Topology/Algebra/InfiniteSum/Order): positivity extension for infinite sums (#21557) …
Added Mathlib.Meta.Positivity.evalTsumView on Github →