mathlib3

13cd3e89 - feat(combinatorics/simple_graph/connectivity): `concat` and `concat_rec` (#17209)

feat(combinatorics/simple_graph/connectivity): `concat` and `concat_rec` (#17209) Adds the alternative constructor for walks along with its recursion principle. (Borrowed from lean2/hott.) Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>