Theorems · Theorem · functional analysis

CStarMatrix.inner_toCLM_conjTranspose_right

∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  [inst_2 : PartialOrder A] [inst_3 : StarOrderedRing A] [inst_4 : Fintype n] {M : CStarMatrix m n A}
  {v : WithCStarModule A (m → A)} {w : WithCStarModule A (n → A)},
  inner A v ((CStarMatrix.toCLM (Matrix.conjTranspose M)) w) = inner A ((CStarMatrix.toCLM M) v) w

Defined in

Mathlib.Analysis.CStarAlgebra.CStarMatrix

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeNonUnitalCStarAlgebraPartialOrderStarOrderedRingFintype