Commit 2023-04-20 12:31 cc2f8464

View on Github →

feat: port AlgebraicTopology.DoldKan.Projections (#3536)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/DoldKan/Projections.lean

added theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self

added theorem AlgebraicTopology.DoldKan.HigherFacesVanish.of_P

added theorem AlgebraicTopology.DoldKan.P_add_Q

added theorem AlgebraicTopology.DoldKan.P_add_Q_f

added theorem AlgebraicTopology.DoldKan.P_f_0_eq

added theorem AlgebraicTopology.DoldKan.P_f_idem

added theorem AlgebraicTopology.DoldKan.P_f_naturality

added theorem AlgebraicTopology.DoldKan.P_idem

added theorem AlgebraicTopology.DoldKan.P_succ

added theorem AlgebraicTopology.DoldKan.P_zero

added def AlgebraicTopology.DoldKan.Q

added theorem AlgebraicTopology.DoldKan.Q_f_0_eq

added theorem AlgebraicTopology.DoldKan.Q_f_idem

added theorem AlgebraicTopology.DoldKan.Q_f_naturality

added theorem AlgebraicTopology.DoldKan.Q_idem

added theorem AlgebraicTopology.DoldKan.Q_succ

added theorem AlgebraicTopology.DoldKan.Q_zero

added theorem AlgebraicTopology.DoldKan.comp_P_eq_self_iff

added theorem AlgebraicTopology.DoldKan.map_P

added theorem AlgebraicTopology.DoldKan.map_Q

added def AlgebraicTopology.DoldKan.natTransP

added def AlgebraicTopology.DoldKan.natTransQ