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