English
The matrix with all columns equal to a given vector u is defined by replicateCol ι w, i.e., the entry at (x, y) equals w x for all x in m and y in ι.
Русский
Матрица с каждым столбцом равным заданному вектору w задаётся как replicateCol ι w, то есть элемент на позиции (x, y) равен w(x) для всех x ∈ m и y ∈ ι.
LaTeX
$$$ (\mathrm{replicateCol}\ ι\ w)_{x y} = w(x) \quad \text{for all } x \in m,\ y \in ι $$$
Lean4
/-- `Matrix.replicateCol ι u` is the matrix with all columns equal to the vector `u`.
To get a column matrix with exactly one column,
`Matrix.replicateCol (Fin 1) u` is the canonical choice.
-/
def replicateCol (ι : Type*) (w : m → α) : Matrix m ι α :=
of fun x _ => w x
