Theorem TopModuleCat.cokerπ_surjective

Modification history

2025-05-19 05:18
Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean
feat: `TopModuleCat` is a `CategoryWithHomology` (#24976) …
Added TopModuleCat.cokerπ_surjectiveView on Github →