Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.idempotents.dold_kan.equivalence_unit_iso

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.equivalence_unit_isoView on Github →