Theorems · Theorem · combinatorics

List.getElem_eq_getElem_rotate

∀ {α : Type u} (l : List α) (n k : ℕ) (hk : k < l.length), l[k] = (l.rotate n)[(l.length - n % l.length + k) % l.length]

A version of List.getElem_rotate that represents l[k] in terms of (List.rotate l n)[⋯], not vice versa. Can be used instead of rewriting List.getElem_rotate from right to left.

Defined in

Mathlib.Data.List.Rotate

Cited by

2 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound