Superscript
📁 Source: Mathlib/Util/Superscript.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsMapping, subscript, toNormal, toSpecial, instHashableChar_mathlib, instInhabitedMapping, default, mkMapping, partitionPoint, satisfyTokensFn, scriptFnNoAntiquot, scriptParser, formatter, parenthesizer, delabSubscript, delabSuperscript, subscript, formatter, parenthesizer, subscriptTerm, formatter, parenthesizer, superscriptTerm, mapStringsM | 24 |
| Theorems | 0 |
| Total | 24 |
Mathlib.Tactic
Definitions
| Name | Category | Theorems |
|---|---|---|
delabSubscript 📖 | CompOp | — |
delabSuperscript 📖 | CompOp | — |
subscript 📖 | CompOp | — |
subscriptTerm 📖 | CompOp | — |
superscriptTerm 📖 | CompOp | — |
Mathlib.Tactic.Superscript
Definitions
| Name | Category | Theorems |
|---|---|---|
Mapping 📖 | CompData | — |
instHashableChar_mathlib 📖 | CompOp | — |
instInhabitedMapping 📖 | CompOp | — |
mkMapping 📖 | CompOp | — |
partitionPoint 📖 | CompOp | — |
satisfyTokensFn 📖 | CompOp | — |
scriptFnNoAntiquot 📖 | CompOp | — |
scriptParser 📖 | CompOp | — |
Mathlib.Tactic.Superscript.Mapping
Definitions
| Name | Category | Theorems |
|---|---|---|
subscript 📖 | CompOp | — |
toNormal 📖 | CompOp | — |
toSpecial 📖 | CompOp | — |
Mathlib.Tactic.Superscript.instInhabitedMapping
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Mathlib.Tactic.Superscript.scriptParser
Definitions
| Name | Category | Theorems |
|---|---|---|
formatter 📖 | CompOp | — |
parenthesizer 📖 | CompOp | — |
Mathlib.Tactic.subscript
Definitions
| Name | Category | Theorems |
|---|---|---|
formatter 📖 | CompOp | — |
parenthesizer 📖 | CompOp | — |
Mathlib.Tactic.superscript
Definitions
| Name | Category | Theorems |
|---|---|---|
formatter 📖 | CompOp | — |
parenthesizer 📖 | CompOp | — |
Std.Format
Definitions
| Name | Category | Theorems |
|---|---|---|
mapStringsM 📖 | CompOp | — |
---