ofLp_toEuclideanLin_apply — Mathlib

English

The action of a matrix on a vector in Euclidean space corresponds to its linear map under toEuclideanLin.

Русский

Действие матрицы над вектором в Евклидовом пространстве соответствует линейному отображению under toEuclideanLin.

LaTeX

$$toEuclideanLin_apply : M v = …$$

Lean4

@[simp]
theorem ofLp_toEuclideanLin_apply (M : Matrix m n 𝕜) (v : EuclideanSpace 𝕜 n) :
    ofLp (toEuclideanLin M v) = M *ᵥ ofLp v :=
  rfl

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