English
If two lists l and l' have the same length, then applying zipWith with any function f and rotating both lists by n yields the same result as rotating the zipped lists: zipWith f l l' rotated by n equals zipWith f (l rotated by n) (l' rotated by n).
Русский
Если два списка l и l' имеют одинаковую длину, то применение zipWith с любой функцией f к этим спискам после поворота на n дает тот же результат, что и поворот попарно полученного списка: zipWith f l l' поворачиваем на n равно zipWith f (l поворот на n) (l' поворот на n).
LaTeX
$$$\\forall {\alpha \beta \gamma} (f:\\alpha \\to \\beta \\to \\gamma) (l:\\mathrm{List}\\alpha) (l':\\mathrm{List}\\beta) (n:\\mathbb{N}) (h:\\ l.length = l'.length), \\mathrm{zipWith} f l l'\\rotate n = \\mathrm{zipWith} f (l\\rotate n) (l'\\rotate n)$$$
Lean4
theorem zipWith_rotate_distrib {β γ : Type*} (f : α → β → γ) (l : List α) (l' : List β) (n : ℕ)
(h : l.length = l'.length) : (zipWith f l l').rotate n = zipWith f (l.rotate n) (l'.rotate n) :=
by
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod, h, zipWith_append,
← drop_zipWith, ← take_zipWith, List.length_zipWith, h, min_self]
rw [length_drop, length_drop, h]
