head?_rotate — Mathlib

English

If n is less than the length of l, the head of l.rotate n equals the nth element of l.

Русский

Если n меньше длины l, то голова списка l.rotate n равна n-й элементу l.

LaTeX

$$$\\forall l\\in\\mathrm{List}\\alpha,\\forall n\\in\\mathbb{N},\\ n < |l| \\Rightarrow head?(l.rotate n) = l[n]?$$$

Lean4

theorem head?_rotate {l : List α} {n : ℕ} (h : n < l.length) : head? (l.rotate n) = l[n]? := by
  rw [head?_eq_getElem?, getElem?_rotate (n.zero_le.trans_lt h), Nat.zero_add, Nat.mod_eq_of_lt h]

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