Theorems · Theorem · functional analysis

DoubleCentralizer.mk.injEq

∀ {𝕜 : 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 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNonUnitalNormedRingNormedSpaceSMulCommClassIsScalarTower