Commit 2023-01-13 18:08 e78a2694

View on Github →

feat: port Data.List.Rotate (#1490)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Rotate.lean

added theorem List.IsRotated.cyclicPermutations

added theorem List.IsRotated.eqv

added theorem List.IsRotated.map

added theorem List.IsRotated.mem_iff

added theorem List.IsRotated.nodup_iff

added theorem List.IsRotated.perm

added theorem List.IsRotated.refl

added theorem List.IsRotated.reverse

added def List.IsRotated.setoid

added theorem List.IsRotated.symm

added theorem List.IsRotated.trans

added def List.IsRotated

added theorem List.Nodup.cyclicPermutations

added theorem List.Nodup.rotate_congr

added theorem List.Nodup.rotate_eq_self_iff

added def List.cyclicPermutations

added theorem List.cyclicPermutations_cons

added theorem List.cyclicPermutations_eq_nil_iff

added theorem List.cyclicPermutations_eq_singleton_iff

added theorem List.cyclicPermutations_nil

added theorem List.cyclicPermutations_of_ne_nil

added theorem List.cyclicPermutations_rotate

added theorem List.isRotated_append

added theorem List.isRotated_comm

added theorem List.isRotated_concat

added theorem List.isRotated_cyclicPermutations_iff

added theorem List.isRotated_iff_mem_map_range

added theorem List.isRotated_iff_mod

added theorem List.isRotated_nil_iff'

added theorem List.isRotated_nil_iff

added theorem List.isRotated_reverse_comm_iff

added theorem List.isRotated_reverse_iff

added theorem List.isRotated_singleton_iff'

added theorem List.isRotated_singleton_iff

added theorem List.length_cyclicPermutations_cons

added theorem List.length_cyclicPermutations_of_ne_nil

added theorem List.length_mem_cyclicPermutations

added theorem List.length_rotate'

added theorem List.length_rotate

added theorem List.map_rotate

added theorem List.mem_cyclicPermutations_iff

added theorem List.mem_cyclicPermutations_self

added theorem List.mem_rotate

added theorem List.nil_eq_rotate_iff

added theorem List.nodup_rotate

added theorem List.nthLe_cyclicPermutations

added theorem List.nthLe_rotate'

added theorem List.nthLe_rotate

added theorem List.nthLe_rotate_one

added theorem List.prod_rotate_eq_one_of_prod_eq_one

added theorem List.reverse_rotate

added theorem List.rotate'_cons_succ

added theorem List.rotate'_eq_drop_append_take

added theorem List.rotate'_length

added theorem List.rotate'_length_mul

added theorem List.rotate'_mod

added theorem List.rotate'_nil

added theorem List.rotate'_rotate'

added theorem List.rotate'_zero

added theorem List.rotate_append_length_eq

added theorem List.rotate_cons_succ

added theorem List.rotate_eq_drop_append_take

added theorem List.rotate_eq_drop_append_take_mod

added theorem List.rotate_eq_iff

added theorem List.rotate_eq_nil_iff

added theorem List.rotate_eq_rotate'

added theorem List.rotate_eq_rotate

added theorem List.rotate_eq_singleton_iff

added theorem List.rotate_injective

added theorem List.rotate_length

added theorem List.rotate_length_mul

added theorem List.rotate_mod

added theorem List.rotate_nil

added theorem List.rotate_perm

added theorem List.rotate_reverse

added theorem List.rotate_rotate

added theorem List.rotate_singleton

added theorem List.rotate_zero

added theorem List.singleton_eq_rotate_iff

added theorem List.zipWith_rotate_distrib

added theorem List.zipWith_rotate_one