mathlib

ff2c9dc3 - feat(combinatorics/simple_graph/connectivity): add functions to split walks and to create paths (#11095)

feat(combinatorics/simple_graph/connectivity): add functions to split walks and to create paths (#11095) This is chunk 3 of #8737. Introduces `take_until` and `drop_until` to split walks at a vertex, `rotate` to rotate cycles, and `to_path` to remove internal redundancy from a walk to create a path with the same endpoints. This also defines a bundled `path` type for `is_path` since `G.path u v` is a useful type.