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,681 to 1,686 of 2,569 results.
MatrixMap.dual_choi_matrix
Mathematical statement
The Choi matrix of the dual map is the transpose of the reindexed Choi matrix of the original map.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.dual_kron
Mathematical statement
The dual of a Kronecker product of maps is the Kronecker product of their duals.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.dual_unique
Mathematical statement
If two matrix maps satisfy the trace duality property, they are equal.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.dual_Unital
Mathematical statement
The dual of TracePreserving map is not trace-preserving, it's unital, that is, M*(I) = I.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.IsCompletelyPositive.comp
Mathematical statement
The composition of IsCompletelyPositive maps is also completely positive.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.IsCompletelyPositive.IsPositive
Project documentation
Definition of a CP map, but with Fintype T in the definition instead of a Fin n. -/ theorem of_Fintype {M : MatrixMap A B R} (h : IsCompletelyPositive M) (T : Type*) [Fintype T] [DecidableEq T] : (M.kron (LinearMap.id : MatrixMap T T R)).IsPositive := by obtain ⟨n, ⟨e⟩⟩ : ∃ n : ℕ, Nonempty (T ≃ Fin n) := Finite.exists_equiv_fin T convert h n using 1 h...
Source project: quantumInfo
Person-level attribution pending.