Theorems · Theorem · functional analysis

DoubleCentralizer.central

∀ {𝕜 : Type u} {A : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (self : DoubleCentralizer 𝕜 A) (x y : A), self.toProd.2 x * y = x * self.toProd.1 y

The centrality condition that the maps linear maps intertwine one another.

Defined in

Mathlib.Analysis.CStarAlgebra.Multiplier

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNonUnitalNormedRingNormedSpaceSMulCommClassIsScalarTower