toMatrix_id_eq_basis_toMatrix — Mathlib

English

The linear equivalence between vector families and matrices is bijective, with explicit inverses given by summing over the basis vectors.

Русский

Линейное эквивалентное отображение между семействами векторов и матрицами биективно, с явными обратными отображениями, заданными суммированием по базисным векторам.

LaTeX

$$def toMatrixEquiv : (ι → M) ≃ₗ[R] Matrix ι ι R with inverse given by invFun m j = ∑ i m i j • e i$$

Lean4

/-- A generalization of `LinearMap.toMatrix_id`. -/
@[simp]
theorem toMatrix_id_eq_basis_toMatrix [Fintype ι] [DecidableEq ι] [Finite ι'] :
    LinearMap.toMatrix b b' id = b'.toMatrix b := by
  ext i
  apply LinearMap.toMatrix_apply

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