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