mathlib3

92395fdf - feat(data/list/rotate): is_rotated (#7299)

feat(data/list/rotate): is_rotated (#7299) `is_rotated l₁ l₂` or `l₁ ~r l₂` asserts that `l₁` and `l₂` are cyclic permutations of each other. This is defined by claiming that `∃ n, l.rotate n = l'`.