sum_toMatrix_smul_self — Mathlib

English

There is a natural linear equivalence between the space of vector-valued functions and the matrix space, given by turning a family into a matrix of coordinates with respect to a basis.

Русский

Существует естественное линейное биективное соответствие между пространством функций векторов и пространством матриц, задаваемое преобразованием семейства в матрицу координат по базису.

LaTeX

$$toMatrixEquiv : (ι → M) ≃ₗ[R] Matrix ι ι R, with left/right inverses given by sums against basis vectors.$$

Lean4

@[simp]
theorem sum_toMatrix_smul_self [Fintype ι] : ∑ i : ι, e.toMatrix v i j • e i = v j := by
  simp_rw [e.toMatrix_apply, e.sum_repr]

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