Percent
📁 Source: Aesop/Percent.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsPercent, fifty, hundred, instBEq, instHPowNat, instLE, instLT, instMul, instOrd, instToString, ofFloat, ofNat, toFloat, toHumanString, δ, instInhabitedPercent, default | 17 |
| Theorems | 0 |
| Total | 17 |
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
Percent 📖 | CompData | — |
instInhabitedPercent 📖 | CompOp | — |
Aesop.Percent
Definitions
| Name | Category | Theorems |
|---|---|---|
fifty 📖 | CompOp | — |
hundred 📖 | CompOp | — |
instBEq 📖 | CompOp | — |
instHPowNat 📖 | CompOp | — |
instLE 📖 | CompOp | — |
instLT 📖 | CompOp | — |
instMul 📖 | CompOp | — |
instOrd 📖 | CompOp | — |
instToString 📖 | CompOp | — |
ofFloat 📖 | CompOp | — |
ofNat 📖 | CompOp | — |
toFloat 📖 | CompOp | — |
toHumanString 📖 | CompOp | — |
δ 📖 | CompOp | — |
Aesop.instInhabitedPercent
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---