Def Mathlib.Meta.Positivity.evalFinsetProd

Modification history

2024-05-07 23:13
Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
feat: Positivity extension for `Finset.prod` (#9365) …
Added Mathlib.Meta.Positivity.evalFinsetProdView on Github →