replicate_succ — Mathlib

English

For any type α, any natural n, and any value a ∈ α, the vector that repeats a exactly n+1 times equals the vector obtained by placing a at the front of the vector that repeats a exactly n times.

Русский

Для любого типа α, любого натурального n и значения a ∈ α вектор, повторяющий a n+1 раз, равен вектору, получаемому добавлением a в начало вектора, который повторяет a n раз.

LaTeX

$$$\\operatorname{replicate}(n+1, a) = \\operatorname{cons}(a, \\operatorname{replicate}(n, a))$$$

Lean4

@[simp]
theorem replicate_succ (val : α) : replicate (n + 1) val = val ::ᵥ (replicate n val) :=
  rfl

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