piLp_ofLp_toEuclideanLin — Mathlib

English

The Euclidean linear map corresponding to a matrix equals the corresponding linear map given by toLin with the standard basis.

Русский

Линейное отображение Евклидова пространства, соответствующее матрице, равно линейному отображению, образованному через toLin с базисами.

LaTeX

$$$toEuclideanLin = toLin (PiLp.basisFun _ _).toBasis (PiLp.basisFun _ _).toBasis$$$

Lean4

@[simp]
theorem piLp_ofLp_toEuclideanLin (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) :
    ofLp (Matrix.toEuclideanLin A x) = Matrix.toLin' A (ofLp x) :=
  rfl

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