Theorems · Theorem · functional analysis

WithCStarModule.pi_norm

∀ {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)] (x : WithCStarModule A ((i : ι) → E i)),
  ‖x‖ = √‖∑ i, inner A (x i) (x i)‖

Defined in

Mathlib.Analysis.CStarAlgebra.Module.Constructions

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraPartialOrderFintypeNormedAddCommGroupModuleSMulCStarModule