Documentation Verification Report

LowDegree

📁 Source: ClassFieldTheory/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean

Statistics

MetricCount
Definitions0
TheoremsH1_isZero_of_trivial, H2π_comp_H2Iso_hom, H2π_comp_H2Iso_hom_apply, H2π_comp_H2Iso_hom_assoc, coe_add, coe_mk', coe_zero
7
Total7

groupCohomology

Theorems

NameKindAssumesProvesValidatesDepends On
H1_isZero_of_trivial 📖
H2π_comp_H2Iso_hom 📖
H2π_comp_H2Iso_hom_apply 📖H2π_comp_H2Iso_hom
H2π_comp_H2Iso_hom_assoc 📖H2π_comp_H2Iso_hom

groupCohomology.cocycles₂

Theorems

NameKindAssumesProvesValidatesDepends On
coe_add 📖
coe_mk' 📖
coe_zero 📖

---

← Back to Index