rotate_eq_self_iff — Mathlib

English

For a nodup list l, l.rotate n = l iff n mod length(l) = 0 or l = [].

Русский

Для списка без повторений l, l.rotate n = l эквивалентно n mod длина(l) = 0 или l = [].

LaTeX

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

Lean4

theorem rotate_eq_self_iff {l : List α} (hl : l.Nodup) {n : ℕ} : l.rotate n = l ↔ n % l.length = 0 ∨ l = [] := by
  rw [← zero_mod, ← hl.rotate_congr_iff, rotate_zero]

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