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 filtersMState.Ket.IsProd_iff_rank_eq_one
Plain-language statement
A ket on a product space is a product state if and only if its coefficient matrix has rank 1.
Source project: quantumInfo
Person-level attribution pending.
MState.multiset_spectrum_relabel_eq
Plain-language statement
The multiset of values in the spectrum of a relabeled state is the same as the multiset of values in the spectrum of the original state.
Source project: quantumInfo
Person-level attribution pending.
MState.no_cloning
Project documentation
The No-cloning theorem, saying that if states ψ and φ can both be perfectly cloned using a unitary U and a fiducial state f, and they aren't identical (their inner product is less than 1), then the two states must be orthogonal to begin with. In short: only orthogonal states can be simultaneously cloned.
Source project: quantumInfo
Person-level attribution pending.
MState.PosDef_mix_of_ne_one
Plain-language statement
If the second state is positive definite and the mixture is nondegenerate, their mixture is also positive definite.
Source project: quantumInfo
Person-level attribution pending.
MState.pure_iff_rank_eq_one
Plain-language statement
A mixed state is pure if and only if its rank is 1.
Source project: quantumInfo
Person-level attribution pending.
MState.pure_of_constant_spectrum
Plain-language statement
If the specturm of a mixed state is (1,0,0...) i.e. a constant distribution, it is a pure state.
Source project: quantumInfo
Person-level attribution pending.