Documentation Verification Report

Trivial

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

Statistics

Metric	Count
Definitions `tateH0TrivIntAddEquivQuotCard`, `tateH0TrivIntEquivZModCard`	2
Theorems `herbrandQuotient_trivial_int_eq_card`, `card_tateH0_trivial_int`, `herbrandQuotient_trivial_int_eq_card`, `instSubsingletonSubtypeIntMemSubmoduleTateZNeg1Trivial`, `instSubsingletonTateHNeg1IntTrivial`, `oneSubGen_trivial_int_eq_zero`, `tateB0_trivial_int_eq_span_card`, `tateZ0_trivial_int_eq_top`	8
Total	10

Rep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`herbrandQuotient_trivial_int_eq_card` 📖	mathematical	—	`herbrandQuotient`	—	`trivial.eq_1` `herbrandQuotient_of` `Representation.herbrandQuotient_trivial_int_eq_card`

Representation

Definitions

Name	Category	Theorems
`tateH0TrivIntAddEquivQuotCard` 📖	CompOp	—
`tateH0TrivIntEquivZModCard` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_tateH0_trivial_int` 📖	mathematical	—	`TateH0`	—	—
`herbrandQuotient_trivial_int_eq_card` 📖	mathematical	—	`herbrandQuotient`	—	`card_tateH0_trivial_int` `instSubsingletonTateHNeg1IntTrivial`
`instSubsingletonSubtypeIntMemSubmoduleTateZNeg1Trivial` 📖	mathematical	—	`tateZNeg1`	—	`norm_trivial_int_eq_card`
`instSubsingletonTateHNeg1IntTrivial` 📖	mathematical	—	`TateHNeg1`	—	`instSubsingletonSubtypeIntMemSubmoduleTateZNeg1Trivial`
`oneSubGen_trivial_int_eq_zero` 📖	mathematical	—	`oneSubGen`	—	—
`tateB0_trivial_int_eq_span_card` 📖	mathematical	—	`tateB0`	—	`norm_trivial_int_eq_card`
`tateZ0_trivial_int_eq_top` 📖	mathematical	—	`tateZ0`	—	`oneSubGen_trivial_int_eq_zero`

---

← Back to Index