Def CochainComplex.mkAux

Modification history

2024-03-13 12:48

Mathlib/Algebra/Homology/HomologicalComplex.lean

perf(Abelian.InjectiveResolution): refactor `CochainComplex.mkAux` (#11349) …

Modified CochainComplex.mkAux View on Github →

2024-01-08 09:51

Mathlib/Algebra/Homology/HomologicalComplex.lean

chore(*): use α → β instead of ∀ _ : α, β (#9529)

Modified CochainComplex.mkAux View on Github →

2023-04-17 19:17

Mathlib/Algebra/Homology/HomologicalComplex.lean

feat: port Algebra.Homology.HomologicalComplex (#3451)

Added CochainComplex.mkAux View on Github →