2025-10-29 16:18
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
feat(Combinatorics/SimpleGraph/Connectivity/WalkCounting): a spanning subgraph has the same or more connected components (#30354)
Added SimpleGraph.ConnectedComponent.surjective_map_ofLE