Small
📁 Source: Mathlib/Data/DFinsupp/Small.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
| 2 | |
| Total | 2 |
DFinsupp
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
small 📖 | mathematical | Small | DFinsupp | — | small_of_injectivesmall_Piext |
Finsupp
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
small 📖 | mathematical | — | SmallFinsupp | — | small_mapDFinsupp.small |
---