rotate_eq_rotate' — Mathlib

English

A small simplification instance relating rotate' and length; a trivial identity used by simplification rules.

Русский

Крохотный случай упрощения между rotate' и длиной; тривиальное тождество для правил упрощения.

LaTeX

$$$\\text{(simp compatible identity for rotate' involving length)}$$$

Lean4

theorem rotate_eq_rotate' (l : List α) (n : ℕ) : l.rotate n = l.rotate' n :=
  if h : l.length = 0 then by simp_all [length_eq_zero_iff]
  else by
    rw [← rotate'_mod, rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))]
    simp [rotate]

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