mathlib

d29aca84 - feat(algebraic_topology/dold_kan): technical lemmas about face maps (#14044)

feat(algebraic_topology/dold_kan): technical lemmas about face maps (#14044) This PR introduces technical lemmas about face maps and the null homotopic maps Hσ that will be used in the proof of the Dold-Kan equivalence. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>