toEuclideanLin_eq_toLin — Mathlib

English

The equality of the Euclidean linear map and the Lin map built from basisFun of orthonormal basis.

Русский

Равенство Евклидова линейного отображения и отображения, построенного по basisFun ортонормированного базиса.

LaTeX

$$$toEuclideanLin = toLin (basisFun n 𝕜).toBasis (basisFun m 𝕜).toBasis$$$

Lean4

theorem toEuclideanLin_eq_toLin [Finite m] :
    (toEuclideanLin : Matrix m n 𝕜 ≃ₗ[𝕜] _) = Matrix.toLin (PiLp.basisFun _ _ _) (PiLp.basisFun _ _ _) :=
  rfl

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