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 115 research declarations. Search 10,000 more complete Mathlib declarations.
115 results
Clear filtersMatrixMap.choi_of_kraus_R
Plain-language statement
The Choi matrix of a map in symmetric Kraus form is a sum of rank-1 projectors.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.dual_choi_matrix
Plain-language 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
Plain-language 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
Plain-language statement
If two matrix maps satisfy the trace duality property, they are equal.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.dual_Unital
Plain-language 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
Plain-language statement
The composition of IsCompletelyPositive maps is also completely positive.
Source project: quantumInfo
Person-level attribution pending.