Theorems · Theorem · functional analysis

CompletelyPositiveMap.mk.sizeOf_spec

∀ {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₂]
  [inst_6 : SizeOf A₁] [inst_7 : SizeOf A₂] (toLinearMap : A₁ →ₗ[ℂ] A₂)
  (map_cstarMatrix_nonneg' : ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap),
  sizeOf { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' } = 1 + sizeOf toLinearMap

Defined in

Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraNonUnitalCStarAlgebraPartialOrderPartialOrderStarOrderedRingStarOrderedRingSizeOfSizeOf