rotate_congr — Mathlib

English

The rotated relation is reflexive: every list is rotated to itself with offset 0.

Русский

Отношение вращения рефлексивно: каждый список вращается сам к себе при смещении 0.

LaTeX

$$$\\forall l:\\mathrm{List}\\alpha, \\ l ~r\\;\\l$$

Lean4

theorem rotate_congr {l : List α} (hl : l.Nodup) (hn : l ≠ []) (i j : ℕ) (h : l.rotate i = l.rotate j) :
    i % l.length = j % l.length := by
  rw [← rotate_mod l i, ← rotate_mod l j] at h
  simpa only [head?_rotate, mod_lt, length_pos_of_ne_nil hn, getElem?_eq_getElem, Option.some_inj, hl.getElem_inj_iff,
    Fin.ext_iff] using congr_arg head? h

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