From 770155071dffa70f904e64a7b34b864058b97688 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 6 May 2026 06:14:14 +0100
Subject: [PATCH 1/2] feat(QuantumMechanics): Add TODO item for QM

---
 .../FiniteTarget/HilbertSpace.lean              | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/Physlib/QuantumMechanics/FiniteTarget/HilbertSpace.lean b/Physlib/QuantumMechanics/FiniteTarget/HilbertSpace.lean
index 7c9154db5..f68bafb81 100644
--- a/Physlib/QuantumMechanics/FiniteTarget/HilbertSpace.lean
+++ b/Physlib/QuantumMechanics/FiniteTarget/HilbertSpace.lean
@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Mathlib.Analysis.InnerProductSpace.PiL2
+public import Physlib.Meta.TODO
 /-!
 
 # The Hilbert space of a finite target quantum mechanical system
@@ -16,6 +17,22 @@ public import Mathlib.Analysis.InnerProductSpace.PiL2
 
 namespace QuantumMechanics
 
+TODO "To match this with the results currently in the `QuantumInfo` part of the library,
+  we should:
+  1. Define `FiniteHilbertSpace` as a structure with a single entry `val`, this
+    should take as an input a finite and decidable type `d`. Below this type is
+    taken as default to be `Fin n`.
+  2. On this type we should then define the structure of an inner-product space, and a
+    Hilbert space.
+  3. We could then define the notation `𝓗[d]` to denote the Hilbert space corresponding
+    to the type `d`.
+  4. The results from `QuantumInfo/Finite/Braket.lean` can then be moved over
+    to Physlib, and related to the definition of the Hilbert space here.
+  Optional. Maybe it is worth moving these files to a directory called `States`, with
+  the idea that it includes this definition of the Hilbert space, the
+  definition of bras and kets, and the definition of mixed states. Maybe also
+  parts of `./ResourceTheory/FreeState`."
+
 /-- The finite dimensional Hilbert space of dimension `n`. -/
 def FiniteHilbertSpace (n : ℕ) : Type := EuclideanSpace ℂ (Fin n)
 

From ad853a633b44f89b1a9d67578c537903f0aca379 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 6 May 2026 06:21:08 +0100
Subject: [PATCH 2/2] refactor: Fix import

---
 Physlib/QuantumMechanics/FiniteTarget/HilbertSpace.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Physlib/QuantumMechanics/FiniteTarget/HilbertSpace.lean b/Physlib/QuantumMechanics/FiniteTarget/HilbertSpace.lean
index f68bafb81..54c572ba1 100644
--- a/Physlib/QuantumMechanics/FiniteTarget/HilbertSpace.lean
+++ b/Physlib/QuantumMechanics/FiniteTarget/HilbertSpace.lean
@@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Mathlib.Analysis.InnerProductSpace.PiL2
-public import Physlib.Meta.TODO
+public import Physlib.Meta.TODO.Basic
 /-!
 
 # The Hilbert space of a finite target quantum mechanical system