Documentation Verification Report

Core

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

Statistics

Metric	Count
Definitions `Entry`, `PositivityExt`, `eval`, `Strictness`, `toNonneg`, `toNonzero`, `toPositive`, `toString`, `bestResult`, `catchNone`, `compareHyp`, `compareHypEq`, `compareHypLE`, `compareHypLT`, `core`, `instReprStrictness`, `repr`, `mkPositivityExt`, `normNumPositivity`, `orElse`, `positivityCanon`, `positivityExt`, `proveNonneg`, `solve`, `throwNone`	25
Theorems `nonneg_of_isNNRat`, `nonneg_of_isNat`, `nonneg_of_isNat'`, `nonneg_of_isRat`, `nz_of_isNegNat`, `nz_of_isRat`, `pos_of_isNNRat`, `pos_of_isNat`, `pos_of_isNat'`, `pos_of_isRat`, `ne_of_ne_of_eq'`	11
Total	36

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`Entry` 📖	CompOp	—
`PositivityExt` 📖	CompData	—
`Strictness` 📖	CompData	—
`bestResult` 📖	CompOp	—
`catchNone` 📖	CompOp	—
`compareHyp` 📖	CompOp	—
`compareHypEq` 📖	CompOp	—
`compareHypLE` 📖	CompOp	—
`compareHypLT` 📖	CompOp	—
`core` 📖	CompOp	—
`instReprStrictness` 📖	CompOp	—
`mkPositivityExt` 📖	CompOp	—
`normNumPositivity` 📖	CompOp	—
`orElse` 📖	CompOp	—
`positivityCanon` 📖	CompOp	—
`positivityExt` 📖	CompOp	—
`proveNonneg` 📖	CompOp	—
`solve` 📖	CompOp	—
`throwNone` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonneg_of_isNNRat` 📖	mathematical	`Mathlib.Meta.NormNum.IsNNRat`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Nat.cast_zero` `MulZeroClass.zero_mul`
`nonneg_of_isNat` 📖	mathematical	`Mathlib.Meta.NormNum.IsNat` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Mathlib.Meta.NormNum.IsNat.to_eq` `Nat.cast_nonneg`
`nonneg_of_isNat'` 📖	mathematical	`Mathlib.Meta.NormNum.IsNat`	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`Mathlib.Meta.NormNum.IsNat.to_eq` `Nat.cast_nonneg'`
`nonneg_of_isRat` 📖	mathematical	`Mathlib.Meta.NormNum.IsRat`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Int.cast_zero` `MulZeroClass.zero_mul`
`nz_of_isNegNat` 📖	—	`Mathlib.Meta.NormNum.IsInt`	—	—	`Mathlib.Meta.NormNum.IsInt.neg_to_eq` `ne_of_gt` `IsStrictOrderedRing.toIsOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero`
`nz_of_isRat` 📖	—	`Mathlib.Meta.NormNum.IsRat`	—	—	`pos_invOf_of_invertible_cast` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Int.cast_lt_zero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `mul_neg_of_neg_of_pos` `IsStrictOrderedRing.toMulPosStrictMono` `ne_iff_lt_or_gt`
`pos_of_isNNRat` 📖	mathematical	`Mathlib.Meta.NormNum.IsNNRat`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`pos_invOf_of_invertible_cast` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Nat.cast_pos` `IsStrictOrderedRing.toIsOrderedRing` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono`
`pos_of_isNat` 📖	mathematical	`Mathlib.Meta.NormNum.IsNat` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Mathlib.Meta.NormNum.IsNat.to_eq` `Nat.cast_pos`
`pos_of_isNat'` 📖	mathematical	`Mathlib.Meta.NormNum.IsNat`	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`Mathlib.Meta.NormNum.IsNat.to_eq` `Nat.cast_pos'`
`pos_of_isRat` 📖	mathematical	`Mathlib.Meta.NormNum.IsRat`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`pos_invOf_of_invertible_cast` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Int.cast_pos` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono`

Mathlib.Meta.Positivity.PositivityExt

Definitions

Name	Category	Theorems
`eval` 📖	CompOp	—

Mathlib.Meta.Positivity.Strictness

Definitions

Name	Category	Theorems
`toNonneg` 📖	CompOp	—
`toNonzero` 📖	CompOp	—
`toPositive` 📖	CompOp	—
`toString` 📖	CompOp	—

Mathlib.Meta.Positivity.instReprStrictness

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ne_of_ne_of_eq'` 📖	—	—	—	—	—

---

← Back to Index