toLin_toMatrix — Mathlib

English

A compatibility statement: the matrix of v equals the matrix obtained by applying the matrix-to-map construction to e and the basis-constr.

Русский

Совместимость: матрица v равна матрице, полученной применением конструктора матрицы к e и базисному конструктору.

LaTeX

$$e.toMatrix v = LinearMap.toMatrix e e (e.constr ℕ v)$$

Lean4

@[simp]
theorem toLin_toMatrix [Finite ι] [Fintype ι'] [DecidableEq ι'] (v : Basis ι' R M) :
    Matrix.toLin v e (e.toMatrix v) = LinearMap.id :=
  v.ext fun i => by cases nonempty_fintype ι; rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]

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