Basic

📁 Source: Mathlib/Tactic/Positivity/Basic.lean

Statistics

Metric	Count
Definitions `evalAbs`, `evalAdd`, `evalAscFactorial`, `evalFactorial`, `evalIntCast`, `evalIntDiv`, `evalIntGCD`, `evalIntLCM`, `evalIte`, `evalMap`, `evalMax`, `evalMin`, `evalMul`, `evalNNRatDen`, `evalNNRatNum`, `evalNatAbs`, `evalNatCast`, `evalNatGCD`, `evalNatLCM`, `evalNatSqrt`, `evalNatSucc`, `evalNegPart`, `evalPNatVal`, `evalPosPart`, `evalPow`, `evalPowZeroNat`, `evalRatDen`, `evalRatNum`	28
Theorems `num_ne_zero_of_ne_zero`, `num_pos_of_pos`, `abs_pos_of_ne_zero`, `int_div_nonneg_of_nonneg_of_pos`, `int_div_nonneg_of_pos_of_nonneg`, `int_div_nonneg_of_pos_of_pos`, `int_div_self_pos`, `int_natAbs_pos`, `ite_ne_zero`, `ite_ne_zero_of_ne_zero_of_pos`, `ite_ne_zero_of_pos_of_ne_zero`, `ite_nonneg`, `ite_nonneg_of_nonneg_of_pos`, `ite_nonneg_of_pos_of_nonneg`, `ite_pos`, `le_min_of_le_of_lt`, `le_min_of_lt_of_le`, `max_ne`, `min_ne`, `min_ne_of_lt_of_ne`, `min_ne_of_ne_of_lt`, `num_ne_zero_of_ne_zero`, `num_nonneg_of_nonneg`, `num_pos_of_pos`, `pow_zero_pos`	25
Total	53

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalAbs` 📖	CompOp	—
`evalAdd` 📖	CompOp	—
`evalAscFactorial` 📖	CompOp	—
`evalFactorial` 📖	CompOp	—
`evalIntCast` 📖	CompOp	—
`evalIntDiv` 📖	CompOp	—
`evalIntGCD` 📖	CompOp	—
`evalIntLCM` 📖	CompOp	—
`evalIte` 📖	CompOp	—
`evalMap` 📖	CompOp	—
`evalMax` 📖	CompOp	—
`evalMin` 📖	CompOp	—
`evalMul` 📖	CompOp	—
`evalNNRatDen` 📖	CompOp	—
`evalNNRatNum` 📖	CompOp	—
`evalNatAbs` 📖	CompOp	—
`evalNatCast` 📖	CompOp	—
`evalNatGCD` 📖	CompOp	—
`evalNatLCM` 📖	CompOp	—
`evalNatSqrt` 📖	CompOp	—
`evalNatSucc` 📖	CompOp	—
`evalNegPart` 📖	CompOp	—
`evalPNatVal` 📖	CompOp	—
`evalPosPart` 📖	CompOp	—
`evalPow` 📖	CompOp	—
`evalPowZeroNat` 📖	CompOp	—
`evalRatDen` 📖	CompOp	—
`evalRatNum` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_pos_of_ne_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `abs`	—	`abs_pos`
`int_div_nonneg_of_nonneg_of_pos` 📖	—	—	—	—	`LT.lt.le`
`int_div_nonneg_of_pos_of_nonneg` 📖	—	—	—	—	`LT.lt.le`
`int_div_nonneg_of_pos_of_pos` 📖	—	—	—	—	`LT.lt.le`
`int_div_self_pos` 📖	—	—	—	—	`LT.lt.ne'` `zero_lt_one` `Int.instZeroLEOneClass`
`int_natAbs_pos` 📖	—	—	—	—	`LT.lt.ne'`
`ite_ne_zero` 📖	—	—	—	—	—
`ite_ne_zero_of_ne_zero_of_pos` 📖	—	`Preorder.toLT`	—	—	`ite_ne_zero` `LT.lt.ne'`
`ite_ne_zero_of_pos_of_ne_zero` 📖	—	`Preorder.toLT`	—	—	`ite_ne_zero` `LT.lt.ne'`
`ite_nonneg` 📖	—	—	—	—	—
`ite_nonneg_of_nonneg_of_pos` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`ite_nonneg` `LT.lt.le`
`ite_nonneg_of_pos_of_nonneg` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`ite_nonneg` `LT.lt.le`
`ite_pos` 📖	—	—	—	—	—
`le_min_of_le_of_lt` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT`	`SemilatticeInf.toMin`	—	`le_min` `LT.lt.le`
`le_min_of_lt_of_le` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	`SemilatticeInf.toMin`	—	`le_min` `LT.lt.le`
`max_ne` 📖	—	—	—	—	—
`min_ne` 📖	—	—	—	—	—
`min_ne_of_lt_of_ne` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`min_ne` `LT.lt.ne'`
`min_ne_of_ne_of_lt` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`min_ne` `LT.lt.ne'`
`num_ne_zero_of_ne_zero` 📖	—	—	—	—	`Rat.num_ne_zero`
`num_nonneg_of_nonneg` 📖	—	—	—	—	—
`num_pos_of_pos` 📖	—	—	—	—	`Rat.num_pos`
`pow_zero_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`LT.lt.trans_le` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `Eq.ge` `pow_zero`

Mathlib.Meta.Positivity.NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`num_ne_zero_of_ne_zero` 📖	—	—	—	—	`NNRat.num_ne_zero`
`num_pos_of_pos` 📖	mathematical	`NNRat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringNNRat`	`NNRat.num`	—	`NNRat.num_pos`

---

← Back to Index