Frontend
📁 Source: Mathlib/Tactic/Linarith/Frontend.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsExprMultiMap, find, insert, LinarithConfig, discharger, exfalso, minimize, oracle, preprocessors, splitHypotheses, splitNe, transparency, updateReducibility, applyContrLemma, findLinarithContradiction, getContrLemma, linarithUsedHyps, partitionByTypeIdx, runLinarith, elabLinarithConfig, linarith?, linarithArgsRest, nlinarith, tacticLinarith!_, tacticLinarith?!_, tacticNlinarith!_ | 26 |
| Theorems | 0 |
| Total | 26 |
Mathlib.Tactic
Definitions
| Name | Category | Theorems |
|---|---|---|
elabLinarithConfig 📖 | CompOp | — |
linarith? 📖 | CompOp | — |
linarithArgsRest 📖 | CompOp | — |
nlinarith 📖 | CompOp | — |
tacticLinarith!_ 📖 | CompOp | — |
tacticLinarith?!_ 📖 | CompOp | — |
tacticNlinarith!_ 📖 | CompOp | — |
Mathlib.Tactic.Linarith
Definitions
| Name | Category | Theorems |
|---|---|---|
ExprMultiMap 📖 | CompOp | — |
LinarithConfig 📖 | CompData | — |
applyContrLemma 📖 | CompOp | — |
findLinarithContradiction 📖 | CompOp | — |
getContrLemma 📖 | CompOp | — |
linarithUsedHyps 📖 | CompOp | — |
partitionByTypeIdx 📖 | CompOp | — |
runLinarith 📖 | CompOp | — |
Mathlib.Tactic.Linarith.ExprMultiMap
Definitions
| Name | Category | Theorems |
|---|---|---|
find 📖 | CompOp | — |
insert 📖 | CompOp | — |
Mathlib.Tactic.Linarith.LinarithConfig
Definitions
| Name | Category | Theorems |
|---|---|---|
discharger 📖 | CompOp | — |
exfalso 📖 | CompOp | — |
minimize 📖 | CompOp | — |
oracle 📖 | CompOp | — |
preprocessors 📖 | CompOp | — |
splitHypotheses 📖 | CompOp | — |
splitNe 📖 | CompOp | — |
transparency 📖 | CompOp | — |
updateReducibility 📖 | CompOp | — |
---