Commit 2025-06-24 15:10 bd0178c4

View on Github →

fix: remove unused DecidableEq arguments (#26352) One proof needed this, but should have used classical instead. This propagated to huge swathes of API.

Estimated changes

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

modified def groupCohomology.inhomogeneousCochainsIso

modified def groupCohomology

modified theorem groupCohomology_induction_on

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

modified theorem groupCohomology.cochainsMap_comp

modified theorem groupCohomology.cocyclesMap_comp

modified theorem groupCohomology.map_comp

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean

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