Mathlib Changelog
v4
Changelog
About
Github
Theorem
coe_connectedComponentsEquivZerothHomotopy_symm
Modification history
2026-02-17 20:49
Mathlib/Topology/Connected/LocPathConnected.lean
feat(Topology/Connected/PathConnected): relate `ZerothHomotopy` and `ConnectedComponents` (#34244)
Added
coe_connectedComponentsEquivZerothHomotopy_symm
View on Github →