Theorems · Theorem · functional analysis

DoubleCentralizer.mk.inj

∀ {𝕜 : 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}
  {toProd : (A →L[𝕜] A) × (A →L[𝕜] A)} {central : ∀ (x y : A), toProd.2 x * y = x * toProd.1 y}
  {toProd_1 : (A →L[𝕜] A) × (A →L[𝕜] A)} {central_1 : ∀ (x y : A), toProd_1.2 x * y = x * toProd_1.1 y},
  { toProd := toProd, central := central } = { toProd := toProd_1, central := central_1 } → toProd = toProd_1

Defined in

Mathlib.Analysis.CStarAlgebra.Multiplier

Cited by

1 results in Mathlib

Foundations

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