Preprocessing
📁 Source: Mathlib/Tactic/Linarith/Preprocessing.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsOrd, cancelDenoms, compWithZero, defaultPreprocessors, filterComparisons, findSquares, flipNegatedComparison, getNatComparisons, isNatCoe, isNatProp, mkNonstrictIntProof, mk_natCast_nonneg_prf, natToInt, nlinarithExtras, normalizeDenominatorsLHS, preprocess, rearrangeComparison, removeNe, removeNe_aux, removeNegations, splitConjunctions, strengthenStrictInt | 22 |
Theoremswithout_one_mul | 1 |
| Total | 23 |
Mathlib.Tactic.Linarith
Definitions
| Name | Category | Theorems |
|---|---|---|
cancelDenoms 📖 | CompOp | — |
compWithZero 📖 | CompOp | — |
defaultPreprocessors 📖 | CompOp | — |
filterComparisons 📖 | CompOp | — |
findSquares 📖 | CompOp | — |
flipNegatedComparison 📖 | CompOp | — |
getNatComparisons 📖 | CompOp | — |
isNatCoe 📖 | CompOp | — |
isNatProp 📖 | CompOp | — |
mkNonstrictIntProof 📖 | CompOp | — |
mk_natCast_nonneg_prf 📖 | CompOp | — |
natToInt 📖 | CompOp | — |
nlinarithExtras 📖 | CompOp | — |
normalizeDenominatorsLHS 📖 | CompOp | — |
preprocess 📖 | CompOp | — |
rearrangeComparison 📖 | CompOp | — |
removeNe 📖 | CompOp | — |
removeNe_aux 📖 | CompOp | — |
removeNegations 📖 | CompOp | — |
splitConjunctions 📖 | CompOp | — |
strengthenStrictInt 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
without_one_mul 📖 | — | MulOne.toMulMulOneClass.toMulOneMulOne.toOne | — | — | one_mul |
Mathlib.Tactic.Linarith.Expr
Definitions
| Name | Category | Theorems |
|---|---|---|
Ord 📖 | CompOp | — |
---