Commit 2023-04-20 10:27 c086651b

View on Github →

feat: port AlgebraicTopology.DoldKan.Faces (#3526)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/DoldKan/Faces.lean

added theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq

added theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero

added theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero

added theorem AlgebraicTopology.DoldKan.HigherFacesVanish.induction

added theorem AlgebraicTopology.DoldKan.HigherFacesVanish.of_comp

added theorem AlgebraicTopology.DoldKan.HigherFacesVanish.of_succ

added def AlgebraicTopology.DoldKan.HigherFacesVanish