English
For a vector m in M, the product b'.toMatrix b · m's representation equals b'.repr m; i.e., matrix times coordinate vector yields the coordinate expression of m in the new basis.
Русский
Для вектора m в M произведение b'.toMatrix b и координатного вектора m даёт координаты m в базисе b'.
LaTeX
$$$\,b'.toMatrix b \; *\!\!\!\! \mathbf{v} = b'.repr(m)$, where $\mathbf{v} = b.repr(m)$$$
Lean4
@[simp]
theorem toMatrix_mulVec_repr [Finite ι'] (m : M) : b'.toMatrix b *ᵥ b.repr m = b'.repr m := by
classical
cases nonempty_fintype ι'
simp [← LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrix_mulVec_repr]