Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.idempotents.dold_kan.hη

Modification history

2023-07-30 10:18

src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean

feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (#17925)

Added category_theory.idempotents.dold_kan.hη View on Github →