Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-20 14:42 aee7bade

View on Github →

feat(data/list/rotate): cyclic_permutations (#8678) For l ~ l' we have list.permutations. We provide the list of cyclic permutations of l such that all members are l ~r l'. This relationship is proven, as well as the induced nodup of the list of cyclic permutants. This also simplifies the cycle.list definition, and removed the requirement for decidable equality in it.

Estimated changes

Modified src/data/list/basic.lean

added theorem list.length_inits

added theorem list.length_tails

added theorem list.nth_le_inits

added theorem list.nth_le_tails

Modified src/data/list/cycle.lean

Modified src/data/list/rotate.lean

added def list.cyclic_permutations

added theorem list.cyclic_permutations_cons

added theorem list.cyclic_permutations_eq_nil_iff

added theorem list.cyclic_permutations_eq_singleton_iff

added theorem list.cyclic_permutations_nil

added theorem list.cyclic_permutations_of_ne_nil

added theorem list.cyclic_permutations_rotate

added theorem list.is_rotated.cyclic_permutations

added theorem list.is_rotated_cyclic_permutations_iff

modified theorem list.is_rotated_nil_iff'

added theorem list.is_rotated_singleton_iff'

added theorem list.is_rotated_singleton_iff

added theorem list.length_cyclic_permutations_cons

added theorem list.length_cyclic_permutations_of_ne_nil

added theorem list.length_mem_cyclic_permutations

added theorem list.mem_cyclic_permutations_iff

added theorem list.mem_cyclic_permutations_self

added theorem list.nil_eq_rotate_iff

added theorem list.nodup.cyclic_permutations

added theorem list.nodup.rotate_congr

added theorem list.nodup.rotate_eq_self_iff

added theorem list.nth_le_cyclic_permutations

added theorem list.rotate_eq_singleton_iff

added theorem list.singleton_eq_rotate_iff