toMatrix_mulVec_repr — Mathlib

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]

Похожие утверждения