Commit 2025-07-19 22:57 5d382e77

View on Github →

fix(RepresentationTheory/Homological/GroupHomology/*): remove unused DecidableEq arguments (#27298) Mirrors #26352. A proof in groupHomology.inhomogeneousChains should use classical rather than a DecidableEq assumption, and this allows us to remove other DecidableEqs too.

Estimated changes

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean

modified def groupHomology.inhomogeneousChainsIso

modified def groupHomologyIso

modified def groupHomologyIsoTor

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean

modified theorem groupHomology.cyclesMap_comp

modified theorem groupHomology.map_comp

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean

modified theorem groupHomology.d₂₁_apply_mem_cycles₁

modified theorem groupHomology.d₃₂_apply_mem_cycles₂

modified theorem groupHomology.isBoundary₀_of_mem_coinvariantsKer