Theorems · Theorem · functional analysis

CStarMatrix.inner_toCLM_conjTranspose_left

∀ {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 (n → A)} {w : WithCStarModule A (m → A)},
  inner A ((CStarMatrix.toCLM (Matrix.conjTranspose M)) v) w = inner A v ((CStarMatrix.toCLM M) w)

Defined in

Mathlib.Analysis.CStarAlgebra.CStarMatrix

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeNonUnitalCStarAlgebraPartialOrderStarOrderedRingFintype