replicate — Mathlib

English

A vector obtained by repeating an element a on length n: replicate(n,a) = ⟨List.replicate n a, List.length_replicate⟩.

Русский

Вектор, полученный повторением элемента a длины n: replicate(n,a) = ⟨List.replicate n a, List.length_replicate⟩.

LaTeX

$$$\\text{replicate }(n,a)=\\langle \\text{List.replicate } n\\ a,\\ \\text{List.length_replicate} \\rangle$$$

Lean4

/-- Vector obtained by repeating an element. -/
def replicate (n : ℕ) (a : α) : Vector α n :=
  ⟨List.replicate n a, List.length_replicate⟩

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