The Hilbert space of a finite target quantum mechanical system

def QuantumMechanics.FiniteHilbertSpace (n : ℕ) : Type

The finite dimensional Hilbert space of dimension n.

Equations

• QuantumMechanics.FiniteHilbertSpace n = EuclideanSpace ℂ (Fin n)

instance QuantumMechanics.instAddCommGroupFiniteHilbertSpace {n : ℕ} : AddCommGroup (FiniteHilbertSpace n)

Equations

• QuantumMechanics.instAddCommGroupFiniteHilbertSpace = inferInstanceAs (AddCommGroup (EuclideanSpace ℂ (Fin n)))

noncomputable instance QuantumMechanics.instModuleComplexFiniteHilbertSpace {n : ℕ} : Module ℂ (FiniteHilbertSpace n)

Equations

• QuantumMechanics.instModuleComplexFiniteHilbertSpace = inferInstanceAs (Module ℂ (EuclideanSpace ℂ (Fin n)))

noncomputable instance QuantumMechanics.instNormedAddCommGroupFiniteHilbertSpace {n : ℕ} : NormedAddCommGroup (FiniteHilbertSpace n)

Equations

• QuantumMechanics.instNormedAddCommGroupFiniteHilbertSpace = inferInstanceAs (NormedAddCommGroup (EuclideanSpace ℂ (Fin n)))

noncomputable instance QuantumMechanics.instInnerProductSpaceComplexFiniteHilbertSpace {n : ℕ} : InnerProductSpace ℂ (FiniteHilbertSpace n)

Equations

• QuantumMechanics.instInnerProductSpaceComplexFiniteHilbertSpace = inferInstanceAs (InnerProductSpace ℂ (EuclideanSpace ℂ (Fin n)))

instance QuantumMechanics.instCompleteSpaceFiniteHilbertSpace {n : ℕ} : CompleteSpace (FiniteHilbertSpace n)