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.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.
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.
MatrixMap.IsCompletelyPositive.of_Fintype
Plain-language statement
Definition of a CP map, but with Fintype T in the definition instead of a Fin n.
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.