mathlib documentation

data.list.rotate

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

source
@[simp]
theorem list.rotate_nil {α : Type u} (n : ℕ) :
list.nil.rotate n = list.nil

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

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

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

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

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

source
theorem list.rotate'_eq_take_append_drop {α : Type u} {l : list α} {n : ℕ} (a : n ≤ l.length) :
l.rotate' n = list.drop n l ++ list.take n l

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

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

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

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

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

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

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

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

source
theorem list.rotate_eq_take_append_drop {α : Type u} {l : list α} {n : ℕ} (a : n ≤ l.length) :
l.rotate n = list.drop n l ++ list.take n l

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

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

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

source
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