2022-11-09 11:34
src/combinatorics/simple_graph/connectivity.lean
feat(combinatorics/simple_graph/connectivity): `fintype G.connected_component` and `decidable G.connected` (#17148) …
Added simple_graph.reachable_iff_exists_finset_walk_length_nonempty