English
Mapping a function f over a rotated list is the same as rotating the mapped list: map f (l.rotate n) = (map f l).rotate n.
Русский
Побочное отображение функции f на повернутый список эквивалентно повороту отображённого списка: map f (l.rotate n) = (map f l).rotate n.
LaTeX
$$$\\forall f:\\alpha \rightarrow \beta,\\forall l:\\mathrm{List}\\alpha,\\forall n:\\mathbb{N}, \\ map f (l.rotate n) = (map f l).rotate n$$$
Lean4
theorem map_rotate {β : Type*} (f : α → β) (l : List α) (n : ℕ) : map f (l.rotate n) = (map f l).rotate n := by
induction n generalizing l with
| zero => simp
| succ n hn =>
rcases l with - | ⟨hd, tl⟩
· simp
· simp [hn]
