mathlib documentation

data.list.rotate

theorem list.rotate_mod {α : Type u} (l : list α) (n : ) :
l.rotate (n % l.length) = l.rotate n

@[simp]
theorem list.rotate_nil {α : Type u} (n : ) :

@[simp]
theorem list.rotate_zero {α : Type u} (l : list α) :
l.rotate 0 = l

@[simp]
theorem list.rotate'_nil {α : Type u} (n : ) :

@[simp]
theorem list.rotate'_zero {α : Type u} (l : list α) :
l.rotate' 0 = l

theorem list.rotate'_cons_succ {α : Type u} (l : list α) (a : α) (n : ) :
(a :: l).rotate' n.succ = (l ++ [a]).rotate' n

@[simp]
theorem list.length_rotate' {α : Type u} (l : list α) (n : ) :

theorem list.rotate'_eq_take_append_drop {α : Type u} {l : list α} {n : } :
n l.lengthl.rotate' n = list.drop n l ++ list.take n l

theorem list.rotate'_rotate' {α : Type u} (l : list α) (n m : ) :
(l.rotate' n).rotate' m = l.rotate' (n + m)

@[simp]
theorem list.rotate'_length {α : Type u} (l : list α) :

@[simp]
theorem list.rotate'_length_mul {α : Type u} (l : list α) (n : ) :
l.rotate' ((l.length) * n) = l

theorem list.rotate'_mod {α : Type u} (l : list α) (n : ) :
l.rotate' (n % l.length) = l.rotate' n

theorem list.rotate_eq_rotate' {α : Type u} (l : list α) (n : ) :
l.rotate n = l.rotate' n

theorem list.rotate_cons_succ {α : Type u} (l : list α) (a : α) (n : ) :
(a :: l).rotate n.succ = (l ++ [a]).rotate n

@[simp]
theorem list.mem_rotate {α : Type u} {l : list α} {a : α} {n : } :
a l.rotate n a l

@[simp]
theorem list.length_rotate {α : Type u} (l : list α) (n : ) :

theorem list.rotate_eq_take_append_drop {α : Type u} {l : list α} {n : } :
n l.lengthl.rotate n = list.drop n l ++ list.take n l

theorem list.rotate_rotate {α : Type u} (l : list α) (n m : ) :
(l.rotate n).rotate m = l.rotate (n + m)

@[simp]
theorem list.rotate_length {α : Type u} (l : list α) :

@[simp]
theorem list.rotate_length_mul {α : Type u} (l : list α) (n : ) :
l.rotate ((l.length) * n) = l

theorem list.prod_rotate_eq_one_of_prod_eq_one {α : Type u} [group α] {l : list α} (hl : l.prod = 1) (n : ) :
(l.rotate n).prod = 1