Commit 2023-04-20 17:11 1d9fdc01

View on Github →

feat: port AlgebraicTopology.DoldKan.PInfty (#3539)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

added theorem AlgebraicTopology.karoubi_alternatingFaceMapComplex_d

deleted theorem AlgebraicTopology.karoubi_alternating_face_map_complex_d

Created Mathlib/AlgebraicTopology/DoldKan/PInfty.lean

added theorem AlgebraicTopology.DoldKan.PInfty_add_QInfty

added theorem AlgebraicTopology.DoldKan.PInfty_comp_QInfty

added theorem AlgebraicTopology.DoldKan.PInfty_f

added theorem AlgebraicTopology.DoldKan.PInfty_f_0

added theorem AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f

added theorem AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f

added theorem AlgebraicTopology.DoldKan.PInfty_f_idem

added theorem AlgebraicTopology.DoldKan.PInfty_f_naturality

added theorem AlgebraicTopology.DoldKan.PInfty_idem

added theorem AlgebraicTopology.DoldKan.P_is_eventually_constant

added theorem AlgebraicTopology.DoldKan.QInfty_comp_PInfty

added theorem AlgebraicTopology.DoldKan.QInfty_f_0

added theorem AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f

added theorem AlgebraicTopology.DoldKan.QInfty_f_idem

added theorem AlgebraicTopology.DoldKan.QInfty_f_naturality

added theorem AlgebraicTopology.DoldKan.QInfty_idem

added theorem AlgebraicTopology.DoldKan.Q_is_eventually_constant

added theorem AlgebraicTopology.DoldKan.karoubi_PInfty_f

added theorem AlgebraicTopology.DoldKan.map_PInfty_f

added theorem AlgebraicTopology.DoldKan.qInfty_f