Def groupHomology.cyclesIso₀

Modification history

2026-09-04 11:59

Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean

chore(CategoryTheory): use the new `↧` notation in concrete categories (#41811) …

Modified groupHomology.cyclesIso₀ View on Github →

2026-03-24 21:13

Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean

chore(RepresentationTheory): Refactor Rep (#36127) …

Modified groupHomology.cyclesIso₀ View on Github →

2025-07-11 11:47

Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean

feat(RepresentationTheory/Homological/GroupHomology/LowDegree): Identify `cycles A n` with `cyclesₙ A` for `n = 0, 1, 2` (#25888) …

Added groupHomology.cyclesIso₀ View on Github →