Hyperquantum state

Different definition of a Quantum state;

import Hypercomplex_numbers

variables (ℋ : Type) [hypercomplex_Hilbert_space ℋ]

/-- linear operator on hypercomplex hilbert space ℋ -/
class hyperquantum_state (ρ : ℋ →ₗ[hyperℂ] ℋ) :=
(trace_one   : Tr ρ = 1)
(pos_semidef : pos_semidef ρ)

Exists non-distillable hyperquantum states with a negative partial transpose;

References

• vanDerEyden2021;