rotate_replicate — Mathlib

English

Rotating a replicated list (replicate n a) by any k leaves it unchanged.

Русский

Вращение повторяющегося списка (replicate n a) любой длины k не меняет его.

LaTeX

$$$\\forall \\alpha \\in \\mathsf{Type},\\forall a \\in \\mathsf{List}(\\alpha),\\forall n,k:\\mathbb{N},\\operatorname{rotate} (\\mathsf{replicate}\\ n\\ a)\\ k = \\mathsf{replicate}\\ n\\ a$$$

Lean4

@[simp]
theorem rotate_replicate (a : α) (n : ℕ) (k : ℕ) : (replicate n a).rotate k = replicate n a :=
  eq_replicate_iff.2 ⟨by rw [length_rotate, length_replicate], fun b hb => eq_of_mem_replicate <| mem_rotate.1 hb⟩

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