Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `herbrandQuotient`, `herbrandQuotient`	2
Theorems `herbrandQuotient_eq_zero`, `herbrandQuotient_ne_zero`, `herbrandQuotient_of`, `herbrandQuotient_ρ`	4
Total	6

Rep

Definitions

Name	Category	Theorems
`herbrandQuotient` 📖	CompOp	8 math math: `herbrandQuotient_isNonarchimedeanLocalField_integer_units`, `herbrandQuotient_of_finite`, `herbrandQuotient_eq_zero`, `herbrandQuotient_isNonarchimedeanLocalField_units`, `herbrandQuotient_eq_of_shortExact`, `herbrandQuotient_ρ`, `herbrandQuotient_trivial_int_eq_card`, `herbrandQuotient_of`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`herbrandQuotient_eq_zero` 📖	mathematical	—	`herbrandQuotient`	—	—
`herbrandQuotient_ne_zero` 📖	—	—	—	—	—
`herbrandQuotient_of` 📖	mathematical	—	`herbrandQuotient` `Representation.herbrandQuotient`	—	`herbrandQuotient.eq_1` `Representation.herbrandQuotient.eq_1`
`herbrandQuotient_ρ` 📖	mathematical	—	`Representation.herbrandQuotient` `herbrandQuotient`	—	—

Representation

Definitions

Name	Category	Theorems
`herbrandQuotient` 📖	CompOp	4 math math: `herbrandQuotient_trivial_int_eq_card`, `herbrandQuotient_of_finite`, `Rep.herbrandQuotient_ρ`, `Rep.herbrandQuotient_of`

---

← Back to Index