isRotated_cyclicPermutations_iff — Mathlib

English

The IsRotated relation between cyclic permutations corresponds exactly to the IsRotated relation between the originals.

Русский

Отношение IsRotated между циклическими перестановками эквивалентно отношению IsRotated между исходными списками.

LaTeX

$$$$l.cyclicPermutations ~r l'.cyclicPermutations \iff l \sim_r l'. $$$$

Lean4

@[simp]
theorem isRotated_cyclicPermutations_iff {l l' : List α} : l.cyclicPermutations ~r l'.cyclicPermutations ↔ l ~r l' := by
  simp only [IsRotated, ← cyclicPermutations_rotate, cyclicPermutations_inj]

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