Commit 2023-04-24 11:35 f339c7df

View on Github →

feat: port AlgebraicTopology.DoldKan.HomotopyEquivalence (#3594)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/DoldKan/HomotopyEquivalence.lean

added def AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex

added def AlgebraicTopology.DoldKan.homotopyPInftyToId

added theorem AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant

added def AlgebraicTopology.DoldKan.homotopyQToZero