Quantum state

/- A Quantum state is a linear operator 
on a complex hilbert space ℋ -/

variables (ℋ : Type) [complex_Hilbert_space ℋ]

class quantum_state (ρ : ℋ →ₗ[ℂ] ℋ) :=
(trace_one   : Tr ρ = 1)
(pos_semidef : pos_semidef ρ)

A Quantum state can be used to model the state of a quantum system.

A Quantum state evolves when it passes through a Quantum channel.

---

Other possible formulations?

• A Hyperquantum state is defined using the field of Hypercomplex numbers instead of complex numbers.

• Real and quaternionic instead of complex quantum theory;