Theorems · Theorem · functional analysis

WithCStarModule.inner_single_left

∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [inst_7 : StarOrderedRing A]
  [inst_8 : DecidableEq ι] (x : WithCStarModule A ((i : ι) → E i)) {i : ι} (y : E i),
  inner A ((WithCStarModule.equiv A ((j : ι) → E j)).symm (Pi.single i y)) x = inner A y (x i)

Defined in

Mathlib.Analysis.CStarAlgebra.Module.Constructions

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraPartialOrderFintypeNormedAddCommGroupModuleSMulCStarModuleStarOrderedRingDecidableEq