SES

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

Statistics

Metric	Count
Definitions herbrandSixTermSequence	1
Theorems herbrandQuotient_eq_of_shortExact, herbrandQuotient_ne_zero_of_shortExact₁, herbrandQuotient_ne_zero_of_shortExact₂, herbrandQuotient_ne_zero_of_shortExact₃, herbrandSixTermSequence_exactAt	5
Total	6

Rep

Definitions

Name	Category	Theorems
herbrandSixTermSequence 📖	CompOp	1 math math: herbrandSixTermSequence_exactAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
herbrandQuotient_eq_of_shortExact 📖	mathematical	—	herbrandQuotient	—	herbrandSixTermSequence_exactAt
herbrandQuotient_ne_zero_of_shortExact₁ 📖	—	—	—	—	herbrandQuotient_ne_zero CategoryTheory.ShortComplex.Exact.moduleCat_finite herbrandSixTermSequence_exactAt
herbrandQuotient_ne_zero_of_shortExact₂ 📖	—	—	—	—	herbrandQuotient_ne_zero CategoryTheory.ShortComplex.Exact.moduleCat_finite herbrandSixTermSequence_exactAt
herbrandQuotient_ne_zero_of_shortExact₃ 📖	—	—	—	—	herbrandQuotient_ne_zero CategoryTheory.ShortComplex.Exact.moduleCat_finite herbrandSixTermSequence_exactAt
herbrandSixTermSequence_exactAt 📖	mathematical	—	herbrandSixTermSequence	—	—

---

← Back to Index