symm — Mathlib

English

The rotation relation on lists is symmetric: if l is a rotation of l', then l' is a rotation of l.

Русский

Отношение вращения списков симметрично: если список l является вращением списка l', то l' является вращением l.

LaTeX

$$$ l \sim_{\mathrm{rot}} l' \Rightarrow l' \sim_{\mathrm{rot}} l $$$

Lean4

@[symm]
theorem symm (h : l ~r l') : l' ~r l := by
  obtain ⟨n, rfl⟩ := h
  rcases l with - | ⟨hd, tl⟩
  · exists 0
  · use (hd :: tl).length * n - n
    rw [rotate_rotate, Nat.add_sub_cancel', rotate_length_mul]
    exact Nat.le_mul_of_pos_left _ (by simp)

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