isRotated_iff_mem_map_range — Mathlib

English

Two lists are rotated iff the second is in the list of all rotates of the first by all shifts up to its length.

Русский

Два списка являются вращениями друг друга тогда и только тогда, когда второй список принадлежит множеству всех вращений первого списка на смещения до его длины.

LaTeX

$$$ l \sim_{\mathrm{rot}} l' \iff l' \in (\text{List.range} (|l|+1)).map (l.rotate) $$

Lean4

theorem isRotated_iff_mem_map_range : l ~r l' ↔ l' ∈ (List.range (l.length + 1)).map l.rotate :=
  by
  simp_rw [mem_map, mem_range, isRotated_iff_mod]
  exact ⟨fun ⟨n, hn, h⟩ => ⟨n, Nat.lt_succ_of_le hn, h⟩, fun ⟨n, hn, h⟩ => ⟨n, Nat.le_of_lt_succ hn, h⟩⟩

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