mathlib3

69d5021b - feat(combinatorics/simple_graph/connectivity): `fintype G.connected_component` and `decidable G.connected` (#17148)

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. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>