Ineq
📁 Source: Mathlib/Data/Ineq.lean
Statistics
| Metric | Count |
|---|---|
Definitionsineq?, ineqOrNotIneq?, cmp, instToFormat, instToString, max, toString, instDecidableEqIneq, instInhabitedIneq, default, instReprIneq, repr | 12 |
| Theorems | 0 |
| Total | 12 |
Lean.Expr
Definitions
| Name | Category | Theorems |
|---|---|---|
ineq? 📖 | CompOp | — |
ineqOrNotIneq? 📖 | CompOp | — |
Mathlib
Definitions
| Name | Category | Theorems |
|---|---|---|
instDecidableEqIneq 📖 | CompOp | — |
instInhabitedIneq 📖 | CompOp | — |
instReprIneq 📖 | CompOp | — |
Mathlib.Ineq
Definitions
| Name | Category | Theorems |
|---|---|---|
cmp 📖 | CompOp | — |
instToFormat 📖 | CompOp | — |
instToString 📖 | CompOp | — |
max 📖 | CompOp | — |
toString 📖 | CompOp | — |
Mathlib.instInhabitedIneq
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Mathlib.instReprIneq
Definitions
| Name | Category | Theorems |
|---|---|---|
repr 📖 | CompOp | — |
---