Theorems · Theorem · functional analysis

CompletelyPositiveMap.mk.injEq

∀ {A₁ : Type u_1} {A₂ : Type u_2} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [inst_3 : PartialOrder A₂] [inst_4 : StarOrderedRing A₁] [inst_5 : StarOrderedRing A₂]
  (toLinearMap : A₁ →ₗ[ℂ] A₂)
  (map_cstarMatrix_nonneg' : ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap)
  (toLinearMap_1 : A₁ →ₗ[ℂ] A₂)
  (map_cstarMatrix_nonneg'_1 : ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap_1),
  ({ toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' } =
      { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 }) =
    (toLinearMap = toLinearMap_1)

Defined in

Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraNonUnitalCStarAlgebraPartialOrderPartialOrderStarOrderedRingStarOrderedRing