toLin_apply — Mathlib

English

Given bases v1 for the domain and v2 for the codomain, and a matrix M, the linear map toLin v1 v2 M sends a vector v to the sum over j of (M.mulVec (v1.repr v) j) times v2 j.

Русский

Дано базисы v1 и v2 и матрица M; отображение toLin v1 v2 M отправляет вектор v в сумму по j: (M.mulVec (v1.repr v) j) · v2 j.

LaTeX

$$$ \\text{toLin}_{v_1,v_2}(M)(v) = \\sum_j (M \\cdot v_1.{\\text{repr}}(v))_j \\; v_{2j} $$$

Lean4

theorem toLin_apply (M : Matrix m n R) (v : M₁) : Matrix.toLin v₁ v₂ M v = ∑ j, (M *ᵥ v₁.repr v) j • v₂ j :=
  show v₂.equivFun.symm (Matrix.toLin' M (v₁.repr v)) = _ by rw [Matrix.toLin'_apply, v₂.equivFun_symm_apply]

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