Theorem Rep.standardComplex.barComplex.d_comp_diagonalSuccIsoFree_inv_eq

Modification history

2025-06-09 08:15
Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
feat(RepresentationTheory/*): add the bar resolution (#21738) …
Added Rep.standardComplex.barComplex.d_comp_diagonalSuccIsoFree_inv_eqView on Github →