Theorem singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopy

Modification history

2026-03-30 09:56
Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean
feat(AlgebraicTopology): homotopy invariance of singular homology (#37091) …
Deleted singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopyView on Github →
2026-03-19 13:59
Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean
feat(AlgebraicTopology/SimplicialObject): define simplicial homotopy (#32881) …
Added singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopyView on Github →