English
The matrix representation of the linear map innerSL with respect to orthonormal bases b and b₂ is vecMulVec(star b₂)(star(b.repr x)).
Русский
Матрица отображения innerSL относительно ортонормированных баз b и b₂ равна vecMulVec(star b₂) (star(b.repr x)).
LaTeX
$$$(innerSL\\,\\mathbb{k}\\, x)_{b,b_2} = \\mathrm{vecMulVec}(\\star b_2)(\\star (b.repr\ \\, x)).$$$
Lean4
/-- The matrix representation of `innerSL 𝕜 x` given by an orthonormal basis `b` and `b₂`
is equal to `vecMulVec (star b₂) (star (b.repr x))`. -/
theorem toMatrix_innerSL_apply [Fintype n] [DecidableEq n] [Fintype m] (b : OrthonormalBasis n 𝕜 E)
(b₂ : OrthonormalBasis m 𝕜 𝕜) (x : E) :
(innerSL 𝕜 x).toMatrix b.toBasis b₂.toBasis = vecMulVec (star b₂) (star (b.repr x)) := by ext;
simp [LinearMap.toMatrix_apply, vecMulVec_apply, OrthonormalBasis.repr_apply_apply, mul_comm]
