toMatrix_eq_toMatrix_constr — Mathlib

English

The equivalence between the matrix representation of a linear map and the matrix built from a basis constraint; this aligns canonical representations with basis coordinates.

Русский

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

LaTeX

$$Equality of matrices: $e$-toMatrix of $v$ equals $LinearMap.toMatrix$ of $e$ with $e.constr$.$$

Lean4

theorem toMatrix_eq_toMatrix_constr [Fintype ι] [DecidableEq ι] (v : ι → M) :
    e.toMatrix v = LinearMap.toMatrix e e (e.constr ℕ v) :=
  by
  ext
  rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]
    -- TODO (maybe) Adjust the definition of `Basis.toMatrix` to eliminate the transpose.

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