Parsing
📁 Source: Mathlib/Tactic/Linarith/Parsing.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsfindDefeq, ExprMap, Monom, lt, one, mul, one, pow, scaleByMonom, SumOfMonom, elimMonom, instOrdMonom, linearFormOfAtom, linearFormOfExpr, linearFormsAndMaxVar, one, scalar, toComp, toCompFold, var, instAddTreeMapOfZeroOfDecidableEq_mathlib | 21 |
| Theorems | 0 |
| Total | 21 |
List
Definitions
| Name | Category | Theorems |
|---|---|---|
findDefeq 📖 | CompOp | — |
Mathlib.Tactic.Linarith
Definitions
| Name | Category | Theorems |
|---|---|---|
ExprMap 📖 | CompOp | — |
Monom 📖 | CompOp | — |
SumOfMonom 📖 | CompOp | — |
elimMonom 📖 | CompOp | — |
instOrdMonom 📖 | CompOp | — |
linearFormOfAtom 📖 | CompOp | — |
linearFormOfExpr 📖 | CompOp | — |
linearFormsAndMaxVar 📖 | CompOp | — |
one 📖 | CompOp | — |
scalar 📖 | CompOp | — |
toComp 📖 | CompOp | — |
toCompFold 📖 | CompOp | — |
var 📖 | CompOp | — |
Mathlib.Tactic.Linarith.Monom
Definitions
| Name | Category | Theorems |
|---|---|---|
lt 📖 | CompOp | — |
one 📖 | CompOp | — |
Mathlib.Tactic.Linarith.Sum
Definitions
| Name | Category | Theorems |
|---|---|---|
mul 📖 | CompOp | — |
one 📖 | CompOp | — |
pow 📖 | CompOp | — |
scaleByMonom 📖 | CompOp | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
instAddTreeMapOfZeroOfDecidableEq_mathlib 📖 | CompOp | — |
---