English
Given a basis e and a family of vectors v: ι' → M, the matrix whose columns are the coordinates of v_j in the basis e equals the matrix of the linear map that sends basis vectors via the construction e.constr.
Русский
Для базиса e и набора векторов v: ι' → M матрица, чьи столбцы состоят из координат v_j в базисе e, совпадает с матрицей линейного отображения, задаваемого конструктором e.constr.
LaTeX
$$$e^{\\text{toMatrix}}(v) = \\text{LinearMap.toMatrix}(e,e)(e\\text{ constr } v)$$$
Lean4
/-- From a basis `e : ι → M` and a family of vectors `v : ι' → M`, make the matrix whose columns
are the vectors `v i` written in the basis `e`. -/
def toMatrix (e : Basis ι R M) (v : ι' → M) : Matrix ι ι' R := fun i j ↦ e.repr (v j) i
