Theorems · Theorem · functional analysis

DoubleCentralizer.norm_fst_eq_snd

∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : StarRing A]
  [CStarRing A] (a : DoubleCentralizer 𝕜 A), ‖a.toProd.1‖ = ‖a.toProd.2‖

For a : 𝓜(𝕜, A), the norms of a.fst and a.snd coincide, and hence these also coincide with ‖a‖ which is max (‖a.fst‖) (‖a.snd‖).

Defined in

Mathlib.Analysis.CStarAlgebra.Multiplier

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNonUnitalNormedRingNormedSpaceSMulCommClassIsScalarTowerStarRingCStarRing