Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,687 to 1,692 of 2,569 results.
MatrixMap.IsCompletelyPositive.of_Fintype
Mathematical statement
Definition of a CP map, but with Fintype T in the definition instead of a Fin n.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.IsPositive.dual
Mathematical statement
The dual of a IsPositive map also IsPositive.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.IsPositive.hermDual
Mathematical statement
The dual of a IsPositive map also IsPositive.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.IsPositive.IsHermitianPreserving
Project documentation
The composition of IsHermitianPreserving maps is also Hermitian preserving. -/ theorem comp {M₁ : MatrixMap A B R} {M₂ : MatrixMap B C R} (h₁ : M₁.IsHermitianPreserving) (h₂ : M₂.IsHermitianPreserving) : IsHermitianPreserving (M₂ ∘ₗ M₁) := fun _ h ↦ h₂ (h₁ h) end IsHermitianPreserving namespace IsPositive variable [Fintype A] [Fintype B] [Fintype C] /- Ev...
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.IsTracePreserving_iff_trace_choi
Mathematical statement
A map is trace preserving iff the partial trace of the Choi matrix is the identity.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.IsTracePreserving.kron
Mathematical statement
The kronecker product of IsTracePreserving maps is also trace preserving.
Source project: quantumInfo
Person-level attribution pending.