Def Mathlib.Meta.Positivity.evalFinsetSum

Modification history

2024-10-20 12:53
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
chore(Algebra/Order/BigOperators/Group/Finset): don't import `Ring` (#17939) …
Modified Mathlib.Meta.Positivity.evalFinsetSumView on Github →
2024-02-22 12:56
Mathlib/Algebra/BigOperators/Order.lean
feat: Positivity extension for `Finset.sum` (#10538) …
Added Mathlib.Meta.Positivity.evalFinsetSumView on Github →