Theorem groupHomology.isBoundary₀_of_mem_coinvariantsKer

Modification history

2025-07-19 22:57
Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean
fix(RepresentationTheory/Homological/GroupHomology/*): remove unused `DecidableEq` arguments (#27298) …
Modified groupHomology.isBoundary₀_of_mem_coinvariantsKerView on Github →
2025-07-10 15:14
Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean
feat(RepresentationTheory/Homological/GroupHomology/LowDegree): add `IsCycle₁` predicate and friends (#25884) …
Added groupHomology.isBoundary₀_of_mem_coinvariantsKerView on Github →