mathlib3

36fceb91 - feat(data/list/cycle): Define `cycle.chain` analog to `list.chain` (#12970)

feat(data/list/cycle): Define `cycle.chain` analog to `list.chain` (#12970) We define `cycle.chain`, which means that a relation holds in all adjacent elements in a cyclic list. We then show that for `r` a transitive relation, `cycle.chain r l` is equivalent to `r` holding for all pairs of elements in `l`.