get_rotate_one — Mathlib

English

For any list l and any k in the rotated by 1 list, (l.rotate 1).get k equals l.get at index (k + 1) mod length(l).

Русский

Для любого списка l и любого k в списке, полученном после поворота на 1, (l.rotate 1).get k равно l.get по индексу (k + 1) mod length(l).

LaTeX

$$$\\forall {\alpha} (l:\\List\\alpha) (k:\\Fin (l.rotate 1).length), \\ (l.rotate 1).get k = l.get \\langle (k.1 + 1) \\% |l|, \\rangle$$$

Lean4

theorem get_rotate_one (l : List α) (k : Fin (l.rotate 1).length) :
    (l.rotate 1).get k = l.get ⟨(k + 1) % l.length, mod_lt _ (length_rotate l 1 ▸ k.pos)⟩ :=
  get_rotate l 1 k

Похожие утверждения