FiniteInfinite
📁 Source: Mathlib/Data/DFinsupp/FiniteInfinite.lean
Statistics
| Metric | Count |
|---|---|
Definitionsfintype | 1 |
| 3 | |
| Total | 4 |
DFinsupp
Definitions
| Name | Category | Theorems |
|---|---|---|
fintype 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
infinite_of_exists_right 📖 | mathematical | — | InfiniteDFinsupp | — | Infinite.of_injectivesingle_injective |
infinite_of_left 📖 | mathematical | Nontrivial | InfiniteDFinsupp | — | Infinite.of_injectivesingle_left_injectiveexists_ne |
infinite_of_right 📖 | mathematical | Infinite | DFinsupp | — | infinite_of_exists_right |
---