Theorems · Theorem · functional analysis

WithCStarModule.norm_single

∀ {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)] [StarOrderedRing A]
  [inst_8 : DecidableEq ι] (i : ι) (y : E i), ‖(WithCStarModule.equiv A ((j : ι) → E j)).symm (Pi.single i y)‖ = ‖y‖

Defined in

Mathlib.Analysis.CStarAlgebra.Module.Constructions

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraPartialOrderFintypeNormedAddCommGroupModuleSMulCStarModuleStarOrderedRingDecidableEq