Def Mathlib.Meta.Positivity.evalNNRatNum

Modification history

2024-05-12 23:39

Mathlib/Tactic/Positivity/Basic.lean

feat: Positivity extension for `NNRat.num`/`NNRat.den` (#12732) …

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