Commit 2022-11-09 11:34 69d5021b
View on Github →feat(combinatorics/simple_graph/connectivity): fintype G.connected_component and decidable G.connected (#17148)
In addition to adding these instances, we generalize the pre-existing fintype instance for walks of a particular length from finite graphs to locally finite graphs.