Theorem SSet.map_ιChainComplex_chainComplexFunctorObjCompMapIso_hom_app_f

Modification history

2026-08-11 15:45
Mathlib/AlgebraicTopology/SimplicialSet/Homology/MapHomologicalComplex.lean
feat(AlgebraicTopology/SimplicialSet/Homology): extension of scalars (#38965) …
Added SSet.map_ιChainComplex_chainComplexFunctorObjCompMapIso_hom_app_fView on Github →