English
The matrix of the map toSpanSingleton R M2 x, with respect to bases v1 and v2, equals vecMulVec (v2.repr x) v1; when v1 is the standard singleton basis, this becomes the column matrix of v2.repr x.
Русский
Матрица отображения toSpanSingleton R M2 x относительно базисов v1 и v2 равна vecMulVec (v2.repr x) v1; когда v1 — стандартный базис единичного типа, это колонная матрица v2.repr x.
LaTeX
$$$\\big(\\text{toSpanSingleton } R M_2 x\\big).toMatrix v_1 v_2 = \\text{vecMulVec} (v_2.repr x) v_1.$$$
Lean4
/-- The matrix of `toSpanSingleton R M₂ x` given by bases `v₁` and `v₂` is equal to
`vecMulVec (v₂.repr x) v₁`. When `v₁ = Module.Basis.singleton`
then this is the column matrix of `v₂.repr x`.` -/
theorem toMatrix_toSpanSingleton (v₁ : Basis n R R) (v₂ : Basis m R M₂) (x : M₂) :
(toSpanSingleton R M₂ x).toMatrix v₁ v₂ = vecMulVec (v₂.repr x) v₁ := by ext;
simp [toMatrix_apply, vecMulVec_apply, mul_comm]
