Documentation Verification Report

ExplicitTate

📁 Source: ClassFieldTheory/Cohomology/FiniteCyclic/ExplicitTate.lean

Statistics

Metric	Count
Definitions `TateH0`, `TateHNeg1`, `oneSubGen`, `tateB0`, `tateBNeg1`, `tateH0LinearEquiv`, `tateH0LinearEquivH2`, `tateHNeg1LinearEquiv`, `tateHNeg1LinearEquivH1`, `tateZ0`, `tateZNeg1`	11
Theorems `tateB0_le_tateZ0`, `tateBNeg1_eq_coinvariantsKer`, `tateBNeg1_le_tateZNeg1`, `tateZ0_eq_invariants`	4
Total	15

Representation

Definitions

Name	Category	Theorems
`TateH0` 📖	CompOp	1 math math: `card_tateH0_trivial_int`
`TateHNeg1` 📖	CompOp	1 math math: `instSubsingletonTateHNeg1IntTrivial`
`oneSubGen` 📖	CompOp	1 math math: `oneSubGen_trivial_int_eq_zero`
`tateB0` 📖	CompOp	2 math math: `tateB0_le_tateZ0`, `tateB0_trivial_int_eq_span_card`
`tateBNeg1` 📖	CompOp	2 math math: `tateBNeg1_eq_coinvariantsKer`, `tateBNeg1_le_tateZNeg1`
`tateH0LinearEquiv` 📖	CompOp	—
`tateH0LinearEquivH2` 📖	CompOp	—
`tateHNeg1LinearEquiv` 📖	CompOp	—
`tateHNeg1LinearEquivH1` 📖	CompOp	—
`tateZ0` 📖	CompOp	3 math math: `tateZ0_trivial_int_eq_top`, `tateB0_le_tateZ0`, `tateZ0_eq_invariants`
`tateZNeg1` 📖	CompOp	2 math math: `instSubsingletonSubtypeIntMemSubmoduleTateZNeg1Trivial`, `tateBNeg1_le_tateZNeg1`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tateB0_le_tateZ0` 📖	mathematical	—	`tateB0` `tateZ0`	—	—
`tateBNeg1_eq_coinvariantsKer` 📖	mathematical	—	`tateBNeg1`	—	`IsCyclic.unique_gen_pow`
`tateBNeg1_le_tateZNeg1` 📖	mathematical	—	`tateBNeg1` `tateZNeg1`	—	—
`tateZ0_eq_invariants` 📖	mathematical	—	`tateZ0`	—	`IsCyclic.gen_generate`

---

← Back to Index