Theorems · Definition · functional analysis

CompletelyPositiveMap.toLinearMap

{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₂] → CompletelyPositiveMap A₁ A₂ → A₁ →ₗ[ℂ] A₂

Defined in

Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraNonUnitalCStarAlgebraPartialOrderPartialOrderStarOrderedRingStarOrderedRing