Delaborators
📁 Source: Mathlib/Util/Delaborators.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsdelabPi, delabPi', piNotation, replacePiNotation, «termΠ__,_», delab_not_in, exists_delab | 7 |
| Theorems | 0 |
| Total | 7 |
PiNotation
Definitions
| Name | Category | Theorems |
|---|---|---|
delabPi 📖 | CompOp | — |
delabPi' 📖 | CompOp | — |
piNotation 📖 | CompOp | — |
replacePiNotation 📖 | CompOp | — |
«termΠ__,_» 📖 | CompOp | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
delab_not_in 📖 | CompOp | — |
exists_delab 📖 | CompOp | — |
---