Theorems · Theorem · functional analysis
CompletelyPositiveMap.map_cstarMatrix_nonneg
∀ {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₂]
{n : Type u_3} [inst_6 : Fintype n] (φ : CompletelyPositiveMap A₁ A₂) (M : CStarMatrix n n A₁), 0 ≤ M → 0 ≤ M.map ⇑φ- Cited by
- 0 results in Mathlib
- Foundations
- Depth 360 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Equivproof · cited by 8,337
- Fintypestatement and proof · cited by 7,736
- PartialOrderstatement and proof · cited by 6,410
- Complexproof · cited by 5,565
- Fintype.cardproof · cited by 1,386
- StarOrderedRingstatement and proof · cited by 587
- NonUnitalCStarAlgebrastatement and proof · cited by 149
- SemilinearMapClass.semilinearMapproof · cited by 80
- CStarMatrixstatement and proof · cited by 67
- StarAlgEquiv.symmproof · cited by 49
- Fintype.equivFinOfCardEqproof · cited by 22
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.