Main results
The main results that the formalization.yaml of FormalFrontier/finite-group-tate-cohomology lists under status.main_results at commit c0c9d563, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.
| Declaration | Kind | Where | Note |
|---|---|---|---|
FiniteGroupTateCohomology.normSequence_exact |
lemma | FiniteGroupTateCohomology/Basic.lean, line 285 | Sorry count 0. Axioms: propext, Classical.choice, Quot.sound. |
FiniteGroupTateCohomology.tateCohomologyNegOneNatIsoKernelNorm |
def | FiniteGroupTateCohomology/Basic.lean, line 352 | Sorry count 0. Axioms: propext, Classical.choice, Quot.sound. |
FiniteGroupTateCohomology.tateCohomologyZeroNatIsoCokernelNorm |
def | FiniteGroupTateCohomology/Basic.lean, line 407 | Sorry count 0. Axioms: propext, Classical.choice, Quot.sound. |
FiniteGroupTateCohomology.Cyclic.tateCohomologyPeriodicity |
def | FiniteGroupTateCohomology/CyclicPeriodicity.lean, line 307 | Sorry count 0. Axioms: propext, Classical.choice, Quot.sound. |
Quoted from the main results in formalization.yaml of FormalFrontier/finite-group-tate-cohomology at commit c0c9d563, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.