Theorems · Theorem · functional analysis

CStarMatrix.toCLM_apply_eq_sum

∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  {M : CStarMatrix m n A} {v : WithCStarModule A (m → A)},
  (CStarMatrix.toCLM M) v = (WithCStarModule.equiv A (n → A)).symm fun j => ∑ i, v i * M i j

Defined in

Mathlib.Analysis.CStarAlgebra.CStarMatrix

Cited by

1 results in Mathlib

Foundations

Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeNonUnitalCStarAlgebra