toEuclideanLin_apply_piLp_toLp — Mathlib

English

Equality of the linear map obtained from Pi-basis correspondence equals the standard basis linear map.

Русский

Равенство линейного отображения, полученного из соответствия базиса Pi, и стандартного базисного отображения.

LaTeX

$$Pi.orthonormalBasis.toBasis ...$$

Lean4

@[simp]
theorem toEuclideanLin_apply_piLp_toLp (M : Matrix m n 𝕜) (v : n → 𝕜) : toEuclideanLin M (toLp _ v) = toLp _ (M *ᵥ v) :=
  rfl

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