Def Mathlib.Meta.Positivity.evalIntegral

Modification history

2025-11-19 06:07
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
chore: move Mathlib to the module system (#31786) …
Deleted Mathlib.Meta.Positivity.evalIntegralView on Github →
2024-03-23 07:28
Mathlib/MeasureTheory/Integral/Bochner.lean
feat: Positivity extension for Bochner integral (#10661) …
Added Mathlib.Meta.Positivity.evalIntegralView on Github →