Datatypes
📁 Source: Mathlib/Tactic/Linarith/Datatypes.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsBranch, CertificateOracle, produceCertificate, ToFormat, add, cmp, coeffOf, coeffs, isContr, scale, str, vars, GlobalBranchingPreprocessor, process, toPreprocessorBase, transform, GlobalPreprocessor, branching, toPreprocessorBase, transform, GlobalPreprocessorToGlobalBranchingPreprocessor, Linexp, add, cmp, contains, get, scale, vars, zfind, Preprocessor, globalize, toPreprocessorBase, transform, PreprocessorBase, description, name, PreprocessorToGlobalBranchingPreprocessor, instInhabitedComp, default, instReprComp, repr, linarithGetProofsMessage, linarithTraceProofs, mkSingleCompZeroOf, parseCompAndExpr | 45 |
| Theorems | 0 |
| Total | 45 |
Mathlib.Tactic.Linarith
Definitions
| Name | Category | Theorems |
|---|---|---|
Branch 📖 | CompOp | — |
CertificateOracle 📖 | CompData | — |
GlobalBranchingPreprocessor 📖 | CompData | — |
GlobalPreprocessor 📖 | CompData | — |
GlobalPreprocessorToGlobalBranchingPreprocessor 📖 | CompOp | — |
Linexp 📖 | CompOp | — |
Preprocessor 📖 | CompData | — |
PreprocessorBase 📖 | CompData | — |
PreprocessorToGlobalBranchingPreprocessor 📖 | CompOp | — |
instInhabitedComp 📖 | CompOp | — |
instReprComp 📖 | CompOp | — |
linarithGetProofsMessage 📖 | CompOp | — |
linarithTraceProofs 📖 | CompOp | — |
mkSingleCompZeroOf 📖 | CompOp | — |
parseCompAndExpr 📖 | CompOp | — |
Mathlib.Tactic.Linarith.CertificateOracle
Definitions
| Name | Category | Theorems |
|---|---|---|
produceCertificate 📖 | CompOp | — |
Mathlib.Tactic.Linarith.Comp
Definitions
| Name | Category | Theorems |
|---|---|---|
ToFormat 📖 | CompOp | — |
add 📖 | CompOp | — |
cmp 📖 | CompOp | — |
coeffOf 📖 | CompOp | — |
coeffs 📖 | CompOp | — |
isContr 📖 | CompOp | — |
scale 📖 | CompOp | — |
str 📖 | CompOp | — |
vars 📖 | CompOp | — |
Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
Definitions
| Name | Category | Theorems |
|---|---|---|
process 📖 | CompOp | — |
toPreprocessorBase 📖 | CompOp | — |
transform 📖 | CompOp | — |
Mathlib.Tactic.Linarith.GlobalPreprocessor
Definitions
| Name | Category | Theorems |
|---|---|---|
branching 📖 | CompOp | — |
toPreprocessorBase 📖 | CompOp | — |
transform 📖 | CompOp | — |
Mathlib.Tactic.Linarith.Linexp
Definitions
| Name | Category | Theorems |
|---|---|---|
add 📖 | CompOp | — |
cmp 📖 | CompOp | — |
contains 📖 | CompOp | — |
get 📖 | CompOp | — |
scale 📖 | CompOp | — |
vars 📖 | CompOp | — |
zfind 📖 | CompOp | — |
Mathlib.Tactic.Linarith.Preprocessor
Definitions
| Name | Category | Theorems |
|---|---|---|
globalize 📖 | CompOp | — |
toPreprocessorBase 📖 | CompOp | — |
transform 📖 | CompOp | — |
Mathlib.Tactic.Linarith.PreprocessorBase
Definitions
| Name | Category | Theorems |
|---|---|---|
description 📖 | CompOp | — |
name 📖 | CompOp | — |
Mathlib.Tactic.Linarith.instInhabitedComp
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Mathlib.Tactic.Linarith.instReprComp
Definitions
| Name | Category | Theorems |
|---|---|---|
repr 📖 | CompOp | — |
---