Theorem CategoryTheory.SimplicialObject.Homotopy.congr_homologyMap_singularChainComplexFunctor

Modification history

2026-04-13 14:38
Mathlib/AlgebraicTopology/SimplicialSet/Homology/HomotopyInvariance.lean
feat(AlgebraicTopology): simplicial homology (#37656) …
Deleted CategoryTheory.SimplicialObject.Homotopy.congr_homologyMap_singularChainComplexFunctorView on Github →
2026-03-30 09:56
Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean
feat(AlgebraicTopology): homotopy invariance of singular homology (#37091) …
Added CategoryTheory.SimplicialObject.Homotopy.congr_homologyMap_singularChainComplexFunctorView on Github →