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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,747 to 1,752 of 2,569 results.
MState.multiset_spectrum_relabel_eq
Mathematical 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
Mathematical 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
Mathematical 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
Mathematical 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.
MState.pure_separable_iff_traceLeft_pure
Mathematical statement
A pure state is separable iff the partial trace on the left is pure.
Source project: quantumInfo
Person-level attribution pending.