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 8 research declarations. Search 10,000 more complete Mathlib declarations.
8 results
Clear filtersMatrixMap.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.IsPositive.dual
Plain-language statement
The dual of a IsPositive map also IsPositive.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.IsPositive.hermDual
Plain-language statement
The dual of a IsPositive map also IsPositive.
Source project: quantumInfo
Person-level attribution pending.