Fintype
📁 Source: Mathlib/Data/FunLike/Fintype.lean
Statistics
| Metric | Count |
|---|---|
| 3 | |
| 2 | |
| Total | 5 |
DFunLike
Definitions
| Name | Category | Theorems |
|---|---|---|
fintype 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
finite 📖 | — | Finite | — | — | Finite.of_injectivePi.finitecoe_injective |
FunLike
Definitions
| Name | Category | Theorems |
|---|---|---|
fintype 📖 | CompOp | — |
toDecidableEq 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
finite 📖 | mathematical | — | Finite | — | DFunLike.finite |
---