Documentation

LeanAPAP.Mathlib.Data.NNRat.Defs

source
def Mathlib.Meta.Positivity.evalNNRatNum :
Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form NNRat.num q, such that positivity successfully recognises q.

Instances For
    source
    def Mathlib.Meta.Positivity.evalNNRatDen :
    Mathlib.Meta.Positivity.PositivityExt

    The positivity extension which identifies expressions of the form Rat.den a.

    Instances For