Finite

📁 Source: ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/Finite.lean

Statistics

Metric	Count
Definitions	0
Theorems herbrandQuotient_of_finite, herbrandQuotient_of_finite	2
Total	2

Rep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
herbrandQuotient_of_finite 📖	mathematical	—	herbrandQuotient	—	herbrandQuotient_ρ Representation.herbrandQuotient_of_finite

Representation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
herbrandQuotient_of_finite 📖	mathematical	—	herbrandQuotient	—	Submodule.natCard_quotient Submodule.natCard_submoduleOf LinearMap.natCard_range_mul_natCard_ker

---

← Back to Index