Commit 2023-04-21 08:03 09aef029

View on Github →

feat: port AlgebraicTopology.DoldKan.Degeneracies (#3561)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean

added theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_σ

added theorem AlgebraicTopology.DoldKan.degeneracy_comp_PInfty

added theorem AlgebraicTopology.DoldKan.σ_comp_PInfty

added theorem AlgebraicTopology.DoldKan.σ_comp_P_eq_zero