FourierMotzkin
📁 Source: Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsfourierMotzkin, CompSource, flatten, toString, LinarithData, comps, maxVar, LinarithM, PComp, add, assump, c, cmp, effective, history, implicit, isContr, maybeMinimal, scale, src, vars, PCompSet, elimAllVarsM, elimVar, elimVarM, elimWithSet, getMaxVar, getPCompSet, instInhabitedCompSource, default, instToFormatCompSource, instToFormatPComp, instToStringPComp, mkLinarithData, pelimVar, splitSetByVarSign, update, validate | 38 |
| Theorems | 0 |
| Total | 38 |
Mathlib.Tactic.Linarith
Definitions
| Name | Category | Theorems |
|---|---|---|
CompSource 📖 | CompData | — |
LinarithData 📖 | CompData | — |
LinarithM 📖 | CompOp | — |
PComp 📖 | CompData | — |
PCompSet 📖 | CompOp | — |
elimAllVarsM 📖 | CompOp | — |
elimVar 📖 | CompOp | — |
elimVarM 📖 | CompOp | — |
elimWithSet 📖 | CompOp | — |
getMaxVar 📖 | CompOp | — |
getPCompSet 📖 | CompOp | — |
instInhabitedCompSource 📖 | CompOp | — |
instToFormatCompSource 📖 | CompOp | — |
instToFormatPComp 📖 | CompOp | — |
instToStringPComp 📖 | CompOp | — |
mkLinarithData 📖 | CompOp | — |
pelimVar 📖 | CompOp | — |
splitSetByVarSign 📖 | CompOp | — |
update 📖 | CompOp | — |
validate 📖 | CompOp | — |
Mathlib.Tactic.Linarith.CertificateOracle
Definitions
| Name | Category | Theorems |
|---|---|---|
fourierMotzkin 📖 | CompOp | — |
Mathlib.Tactic.Linarith.CompSource
Definitions
| Name | Category | Theorems |
|---|---|---|
flatten 📖 | CompOp | — |
toString 📖 | CompOp | — |
Mathlib.Tactic.Linarith.LinarithData
Definitions
| Name | Category | Theorems |
|---|---|---|
comps 📖 | CompOp | — |
maxVar 📖 | CompOp | — |
Mathlib.Tactic.Linarith.PComp
Definitions
| Name | Category | Theorems |
|---|---|---|
add 📖 | CompOp | — |
assump 📖 | CompOp | — |
c 📖 | CompOp | — |
cmp 📖 | CompOp | — |
effective 📖 | CompOp | — |
history 📖 | CompOp | — |
implicit 📖 | CompOp | — |
isContr 📖 | CompOp | — |
maybeMinimal 📖 | CompOp | — |
scale 📖 | CompOp | — |
src 📖 | CompOp | — |
vars 📖 | CompOp | — |
Mathlib.Tactic.Linarith.instInhabitedCompSource
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---