rotate_congr_iff — Mathlib

English

For a nodup list l, if l.rotate i = l.rotate j then i mod length(l) = j mod length(l) or l = [].

Русский

Для неповторяющегося списка l, если l.rotate i = l.rotate j, то i mod длина(l) = j mod длина(l) или l пуст.

LaTeX

$$$\\forall {l: List\\alpha} (hl: l.Nodup) {i j: \\mathbb{N}}, \\ l.rotate i = l.rotate j \\Rightarrow i \\% l.length = j \\% l.length \\lor l = []$$$

Lean4

theorem rotate_congr_iff {l : List α} (hl : l.Nodup) {i j : ℕ} :
    l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = [] :=
  by
  rcases eq_or_ne l [] with rfl | hn
  · simp
  · simp only [hn, or_false]
    refine ⟨hl.rotate_congr hn _ _, fun h ↦ ?_⟩
    rw [← rotate_mod, h, rotate_mod]

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