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 160 research declarations. Search 10,000 more complete Mathlib declarations.
160 results
Clear filtersMatrixMap.IsPositive.hermDual
Plain-language 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
Plain-language 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
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.