get_replicate — Mathlib

English

In a replicated vector of length n with constant value a, every position contains a.

Русский

В векторе длины n, скопированном из одного значения a, во всех позициях содержится a.

LaTeX

$$$\forall i:\mathrm{Fin}\,n,\; (\mathrm{Vector}.\mathrm{replicate}\ n\ a).get\ i = a$$$

Lean4

@[simp]
theorem get_replicate (a : α) (i : Fin n) : (Vector.replicate n a).get i = a := by apply List.getElem_replicate

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