Def Mathlib.Meta.Positivity.Meta.Positivity.proveNonneg

Modification history

2024-11-11 01:53

Mathlib/Tactic/Positivity/Core.lean

feat: extend `linear_combination` to prove inequalities (#16841) …

Added Mathlib.Meta.Positivity.Meta.Positivity.proveNonneg View on Github →