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.IsTracePreserving.kron
Plain-language statement
The kronecker product of IsTracePreserving maps is also trace preserving.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.kron_def
Plain-language statement
The extensional definition of the Kronecker product MatrixMap.kron, in terms of the entries of its image.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.kron_kronecker_const
Plain-language statement
The map that takes M and returns M ⊗ₖ C, where C is positive semidefinite, is a completely positive map.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.kron_map_of_kron_state
Plain-language statement
The operational definition of the Kronecker product MatrixMap.kron, that it maps a Kronecker product of inputs to the Kronecker product of outputs. It is the unique bilinear map doing so.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.Module.Basis.dualMap_toDualEquiv_symm_comp_toDualEquiv
Plain-language statement
The composition of the dual of the inverse of the dual basis isomorphism with the dual basis isomorphism is the evaluation map.
Source project: quantumInfo
Person-level attribution pending.
MatrixMap.Module.Basis.toDualEquiv_symm_comp_dualMap_toDualEquiv
Plain-language statement
The composition of the inverse of the dual basis isomorphism with the dual of the dual basis isomorphism is the inverse of the evaluation map.
Source project: quantumInfo
Person-level attribution pending.