replicateRow — Mathlib

English

The matrix with all rows equal to a given vector v is defined by replicateRow, i.e., the entry at (i, j) equals v j for all i in ι and j in n.

Русский

Матрица с каждым рядом равной заданному вектору v задаётся как replicateRow, то есть элемент на позиции (i, j) равен v(j) для всех i и j.

LaTeX

$$$ (\mathrm{replicateRow}\ ι\ v)_{i j} = v(j) \quad \text{for all } i \in ι,\ j \in n $$$

Lean4

/-- `Matrix.replicateRow ι u` is the matrix with all rows equal to the vector `u`.

To get a row matrix with exactly one row, `Matrix.replicateRow (Fin 1) u` is the canonical choice.
-/
def replicateRow (ι : Type*) (v : n → α) : Matrix ι n α :=
  of fun _ y => v y

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