Theorems · Theorem · functional analysis

DoubleCentralizer.ext

∀ (𝕜 : 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]
  (a b : DoubleCentralizer 𝕜 A), a.toProd = b.toProd → a = b

Defined in

Mathlib.Analysis.CStarAlgebra.Multiplier

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNonUnitalNormedRingNormedSpaceSMulCommClassIsScalarTower