List rotation #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file proves basic results about
list.rotate, the list rotation.
Main declarations #
is_rotated l₁ l₂: States that
l₁is a rotated version of
cyclic_permutations l: The list of all cyclic permutants of
l, up to the length of
rotated, rotation, permutation, cycle
is_rotated l₁ l₂ or
l₁ ~r l₂ asserts that
l₂ are cyclic permutations
of each other. This is defined by claiming that
∃ n, l.rotate n = l'.
List of all cyclic permutations of
cyclic_permutations of a nonempty list
l will always contain
list.length l elements.
This implies that under certain conditions, there are duplicates in
nth entry is equal to
l.rotate n, proven in
The proof that every cyclic permutant of
l is in the list is
cyclic_permutations [1, 2, 3, 2, 4] = [[1, 2, 3, 2, 4], [2, 3, 2, 4, 1], [3, 2, 4, 1, 2], [2, 4, 1, 2, 3], [4, 1, 2, 3, 2]]