toCLM_apply_eq_sum — Mathlib

English

For any M and v, the coordinate-wise action of toCLM equals the sum over i of v_i times the i-th row of M, giving the j-th component.

Русский

Для любых M и v, действия toCLM дают сумму по i от v_i умноженной на i-ю строку M, образующую j-ю компоненту.

LaTeX

$$$toCLM\,M\,v = (\text{WithCStarModule.equiv}_A(n\to A))^{-1} \bigl( \sum_i v_i \cdot M_{i,\cdot} \bigr)$$$

Lean4

theorem toCLM_apply_eq_sum {M : CStarMatrix m n A} {v : C⋆ᵐᵒᵈ(A, m → A)} :
    toCLM M v = (WithCStarModule.equiv _ _).symm (fun j => ∑ i, v i * M i j) :=
  by
  ext i
  simp [toCLM_apply, Matrix.vecMul, dotProduct]

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