rotate_append_length_eq — Mathlib

English

For any lists l and l', rotating the concatenation l ++ l' by l.length yields l' ++ l.

Русский

Для любых списков l и l' вращение конкатенации l ++ l' на длину l даёт l' ++ l.

LaTeX

$$$\\forall l,l'\\in \\mathsf{List}(\\alpha),\\ (l ++ l').rotate(l.length) = l' ++ l$$$

Lean4

@[simp]
theorem rotate_append_length_eq (l l' : List α) : (l ++ l').rotate l.length = l' ++ l :=
  by
  rw [rotate_eq_rotate']
  induction l generalizing l'
  · simp
  · simp_all [rotate']

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