Finite
📁 Source: Mathlib/GroupTheory/Abelianization/Finite.lean
Statistics
| Metric | Count |
|---|---|
| 1 | |
TheoremsinstFiniteAbelianization | 1 |
| Total | 2 |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
instFintypeAbelianizationOfDecidablePredMemSubgroupCommutator 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
instFiniteAbelianization 📖 | mathematical | — | FiniteAbelianization | — | Quotient.finite |
---