diff --git a/Physlib.lean b/Physlib.lean
index 5d704d893..ebd41f77e 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -122,6 +122,8 @@ public import Physlib.Mathematics.LinearPMap
 public import Physlib.Mathematics.List
 public import Physlib.Mathematics.List.InsertIdx
 public import Physlib.Mathematics.List.InsertionSort
+public import Physlib.Mathematics.OneParameterSubgroups.Basic
+public import Physlib.Mathematics.OneParameterSubgroups.Unitary
 public import Physlib.Mathematics.OrthogonalMatrix
 public import Physlib.Mathematics.PiTensorProduct
 public import Physlib.Mathematics.RatComplexNum
diff --git a/Physlib/Mathematics/OneParameterSubgroups/Basic.lean b/Physlib/Mathematics/OneParameterSubgroups/Basic.lean
new file mode 100644
index 000000000..e2fca126a
--- /dev/null
+++ b/Physlib/Mathematics/OneParameterSubgroups/Basic.lean
@@ -0,0 +1,196 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Mathlib.Analysis.Calculus.Deriv.Shift
+public import Mathlib.Analysis.Calculus.MeanValue
+public import Mathlib.Analysis.SpecialFunctions.Exponential
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
+
+/-!
+
+# One-parameter subgroups of real Banach algebras
+
+## i. Overview
+
+Let `E` be a real Banach algebra. This file proves that every continuous additive character
+`U : AddChar ℝ E` has the form `U(t) = exp (t • A)`, where `A = deriv U 0`.
+
+This is the Banach-algebra argument underlying the correspondence between norm-continuous unitary
+one-parameter groups and bounded self-adjoint generators. See
+`Physlib.Mathematics.OneParameterSubgroups.Unitary` for that correspondence.
+
+**Proof outline.** Continuity at zero implies that, for sufficiently small `d > 0`, the integral of
+`U` over `[0, d]` is close to `d • 1` and therefore invertible. If `I` is the indefinite integral of
+`U`, the homomorphism law gives `U(t) * I(d) = I(t + d) - I(t)`. This identity proves that `U` is
+differentiable. Setting `A` to the derivative at zero then gives the differential equation
+`U'(t) = U(t)A`. Consequently `U(t) * exp (-tA)` has zero derivative and is constant. Uniqueness
+follows by differentiating two exponential representations at zero.
+
+## ii. Key results
+
+* `OneParameterSubgroup.apply_eq_exp_smul_deriv`: A continuous one-parameter subgroup is the
+  exponential of its derivative at zero.
+* `OneParameterSubgroup.generator_unique`: Any exponential generator equals the derivative at zero.
+
+## iii. References
+
+-/
+
+@[expose] public section
+
+open Filter Topology
+
+noncomputable section
+
+namespace OneParameterSubgroup
+
+variable {E : Type*} [NormedRing E] [NormedAlgebra ℝ E] [CompleteSpace E]
+
+/-- `NormedSpace.exp`'s API wants a `ℚ`-algebra structure (for the `1/n!` coefficients), which
+isn't automatic from `NormedAlgebra ℝ E` alone; derive it once here rather than at each use site. -/
+local instance : NormedAlgebra ℚ E := .restrictScalars ℚ ℝ E
+
+lemma exists_isUnit_intervalIntegral [Nontrivial E] (U : AddChar ℝ E) (hU : Continuous U) :
+    ∃ d : ℝ, 0 < d ∧ IsUnit (∫ x in (0 : ℝ)..d, U x) := by
+  let c : ℝ := ‖(1 : E)‖⁻¹ / 2
+  have hone : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero
+  have hc : 0 < c := by dsimp [c]; positivity
+  have hevent : ∀ᶠ x : ℝ in 𝓝 0, ‖U x - 1‖ < c := by
+    have hnorm : Continuous (fun x : ℝ => ‖U x - 1‖) :=
+      continuous_norm.comp (hU.sub continuous_const)
+    have hmem : Set.Iio c ∈ 𝓝 ‖U 0 - 1‖ := by simpa using Iio_mem_nhds hc
+    exact hnorm.continuousAt hmem
+  rw [Metric.eventually_nhds_iff] at hevent
+  obtain ⟨r, hr, hrU⟩ := hevent
+  let d := r / 2
+  have hd : 0 < d := by dsimp [d]; positivity
+  let q : Eˣ := {
+    val := d • 1
+    inv := d⁻¹ • 1
+    val_inv := by rw [smul_mul_smul_comm, mul_inv_cancel₀ hd.ne', one_smul, one_mul]
+    inv_val := by rw [smul_mul_smul_comm, inv_mul_cancel₀ hd.ne', one_smul, one_mul] }
+  refine ⟨d, hd, (Units.ofNearby q _ ?_).isUnit⟩
+  calc
+    ‖(∫ x in (0 : ℝ)..d, U x) - (q : E)‖ =
+        ‖(∫ x in (0 : ℝ)..d, U x) - d • (1 : E)‖ := rfl
+    _ = ‖(∫ x in (0 : ℝ)..d, U x) - ∫ _x in (0 : ℝ)..d, (1 : E)‖ := by
+      rw [intervalIntegral.integral_const, sub_zero]
+    _ = ‖∫ x in (0 : ℝ)..d, (U x - 1)‖ := by
+      rw [intervalIntegral.integral_sub (hU.intervalIntegrable 0 d)
+        (continuous_const.intervalIntegrable 0 d)]
+    _ ≤ c * d := by
+      calc
+        _ ≤ c * |d - 0| := intervalIntegral.norm_integral_le_of_norm_le_const (fun x hx => by
+          apply le_of_lt
+          apply hrU
+          rw [Real.dist_0_eq_abs]
+          rw [Set.uIoc_of_le hd.le] at hx
+          rw [abs_of_nonneg hx.1.le]
+          exact hx.2.trans_lt (by dsimp [d]; linarith))
+        _ = c * d := by rw [sub_zero, abs_of_pos hd]
+    _ < ‖(↑q⁻¹ : E)‖⁻¹ := by
+      have hright : ‖(↑q⁻¹ : E)‖⁻¹ = d * ‖(1 : E)‖⁻¹ := by
+        change ‖d⁻¹ • (1 : E)‖⁻¹ = _
+        rw [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_pos hd]
+        field_simp
+      rw [hright]
+      dsimp [c]
+      nlinarith [inv_pos.mpr hone]
+
+/-- Translating a one-parameter subgroup translates its interval integral. -/
+lemma mul_intervalIntegral_eq_sub (U : AddChar ℝ E) (hU : Continuous U) (s t : ℝ) :
+    U s * ∫ x in (0 : ℝ)..t, U x =
+      (∫ x in (0 : ℝ)..(s + t), U x) - ∫ x in (0 : ℝ)..s, U x := by
+  let L : E →L[ℝ] E :=
+    (LinearMap.mulLeft ℝ (U s)).mkContinuous ‖U s‖ (fun x => norm_mul_le _ _)
+  calc
+    U s * ∫ x in (0 : ℝ)..t, U x = L (∫ x in (0 : ℝ)..t, U x) := rfl
+    _ = ∫ x in (0 : ℝ)..t, L (U x) :=
+      (L.intervalIntegral_comp_comm (hU.intervalIntegrable 0 t)).symm
+    _ = ∫ x in (0 : ℝ)..t, U (s + x) := by
+      apply intervalIntegral.integral_congr
+      intro x _
+      exact (U.map_add_eq_mul s x).symm
+    _ = ∫ x in s..(s + t), U x := by
+      rw [intervalIntegral.integral_comp_add_left, add_zero]
+    _ = (∫ x in (0 : ℝ)..(s + t), U x) - ∫ x in (0 : ℝ)..s, U x := by
+      rw [eq_sub_iff_add_eq, add_comm]
+      exact intervalIntegral.integral_add_adjacent_intervals
+        (hU.intervalIntegrable 0 s) (hU.intervalIntegrable s (s + t))
+
+lemma differentiable [Nontrivial E] (U : AddChar ℝ E) (hU : Continuous U) :
+    Differentiable ℝ U := by
+  obtain ⟨d, _, hV⟩ := exists_isUnit_intervalIntegral U hU
+  let V : E := ∫ x in (0 : ℝ)..d, U x
+  let v : Eˣ := hV.unit
+  have hv : (v : E) = V := hV.unit_spec
+  let F : ℝ → E := fun t => ∫ x in (0 : ℝ)..t, U x
+  have hF (t : ℝ) : HasDerivAt F (U t) t :=
+    (hU.integral_hasStrictDerivAt 0 t).hasDerivAt
+  have htranslate (t : ℝ) : U t * V = F (t + d) - F t :=
+    mul_intervalIntegral_eq_sub U hU t d
+  intro t
+  have hR : HasDerivAt (fun s : ℝ => F (s + d) - F s)
+      (U (t + d) - U t) t := by
+    exact (HasDerivAt.comp_add_const t d (hF (t + d))).sub (hF t)
+  have heq : U = fun s : ℝ => (F (s + d) - F s) * (↑v⁻¹ : E) := by
+    funext s
+    calc
+      U s = (U s * (v : E)) * (↑v⁻¹ : E) := by simp
+      _ = (F (s + d) - F s) * (↑v⁻¹ : E) := by rw [hv, htranslate]
+  rw [heq]
+  exact (hR.mul_const (↑v⁻¹ : E)).differentiableAt
+
+lemma apply_eq_exp_smul_deriv (U : AddChar ℝ E) (hU : Continuous U) (t : ℝ) :
+    U t = NormedSpace.exp (t • deriv U 0) := by
+  cases subsingleton_or_nontrivial E with
+  | inl _ => exact Subsingleton.elim _ _
+  | inr _ =>
+    have hdiff : Differentiable ℝ U := differentiable U hU
+    let A : E := deriv U 0
+    have hUderiv (t : ℝ) : HasDerivAt U (U t * A) t := by
+      have ht : HasDerivAt U (deriv U t) t :=
+        hdiff.differentiableAt.hasDerivAt
+      have h0 : HasDerivAt U (deriv U 0) 0 :=
+        hdiff.differentiableAt.hasDerivAt
+      have hleft : HasDerivAt (fun s : ℝ => U (t + s)) (deriv U t) 0 :=
+        HasDerivAt.comp_const_add t 0 (by simpa using ht)
+      have hright : HasDerivAt (fun s : ℝ => U t * U s) (U t * A) 0 := by
+        dsimp only [A]
+        exact HasDerivAt.const_mul (U t) h0
+      have heq : (fun s : ℝ => U (t + s)) = fun s : ℝ => U t * U s := by
+        funext s
+        exact U.map_add_eq_mul t s
+      have hder : deriv U t = U t * A := hleft.unique (heq ▸ hright)
+      rwa [← hder]
+    let G : ℝ → E := fun t => U t * NormedSpace.exp (t • (-A))
+    have hG : Differentiable ℝ G := fun t =>
+      ((hUderiv t).mul (hasDerivAt_exp_smul_const (-A) t)).differentiableAt
+    have hGder (t : ℝ) : deriv G t = 0 := by
+      apply ((hUderiv t).mul (hasDerivAt_exp_smul_const (-A) t)).deriv.trans
+      have hcomm : Commute A (NormedSpace.exp (t • (-A))) := by
+        exact ((Commute.refl A).neg_right.smul_right t).exp_right
+      rw [mul_assoc, hcomm.eq]
+      noncomm_ring
+    have hconst (t : ℝ) : G t = G 0 := is_const_of_deriv_eq_zero hG hGder t 0
+    have hone : U t * Ring.inverse (NormedSpace.exp (t • A)) = 1 := by
+      simpa [G, ← Ring.inverse_exp] using hconst t
+    have hexp : IsUnit (NormedSpace.exp (t • A)) := NormedSpace.isUnit_exp (t • A)
+    let e : Eˣ := hexp.unit
+    have he : (e : E) = NormedSpace.exp (t • A) := hexp.unit_spec
+    rw [← he, Ring.inverse_unit] at hone
+    calc
+      U t = (U t * (↑e⁻¹ : E)) * (e : E) := by simp
+      _ = NormedSpace.exp (t • A) := by
+        rw [hone, one_mul, he]
+
+/-- Any exponential generator of a one-parameter subgroup is its derivative at zero. -/
+lemma generator_unique (U : AddChar ℝ E) (A : E)
+    (h : ∀ t : ℝ, U t = NormedSpace.exp (t • A)) : A = deriv U 0 := by
+  simp [funext h, (hasDerivAt_exp_smul_const A (0 : ℝ)).deriv]
+
+end OneParameterSubgroup
diff --git a/Physlib/Mathematics/OneParameterSubgroups/Unitary.lean b/Physlib/Mathematics/OneParameterSubgroups/Unitary.lean
new file mode 100644
index 000000000..42468379a
--- /dev/null
+++ b/Physlib/Mathematics/OneParameterSubgroups/Unitary.lean
@@ -0,0 +1,202 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Mathlib.Analysis.InnerProductSpace.Adjoint
+public import Physlib.Mathematics.OneParameterSubgroups.Basic
+
+/-!
+
+# Unitary one-parameter groups
+
+A norm-continuous unitary one-parameter group on a complex Hilbert space has a unique bounded
+self-adjoint generator. With the convention used here, the group generated by `A` is
+`U(t) = exp (-itA)`.
+
+The same correspondence describes bounded generators of time translations, spatial translations,
+rotations, and other norm-continuous unitary one-parameter groups. The general theorem for strongly
+continuous groups and unbounded generators requires spectral theory that is not yet available in
+Physlib.
+
+## Main results
+
+* `UnitaryOneParameterGroup.generator`: The canonical bounded self-adjoint generator.
+* `UnitaryOneParameterGroup.apply_eq_exp_generator`: The formula `U(t) = exp (-itA)`.
+* `UnitaryOneParameterGroup.ofSelfAdjoint`: The group generated by a bounded self-adjoint operator.
+* `UnitaryOneParameterGroup.stoneEquiv`: Stone's correspondence for bounded generators.
+
+## References
+
+* M. H. Stone, *Linear Transformations in Hilbert Space III. Operational Methods and Group Theory*,
+  Proc. Natl. Acad. Sci. 18 (1932), 172-175.
+
+-/
+
+@[expose] public section
+
+noncomputable section
+
+/-- A norm-continuous unitary one-parameter group on a complex Hilbert space. -/
+structure UnitaryOneParameterGroup (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
+    [CompleteSpace H] where
+  /-- The additive character from the real parameter to unitary operators. -/
+  toAddChar : AddChar ℝ (unitary (H →L[ℂ] H))
+  /-- The group is continuous in the operator norm. -/
+  continuous : Continuous toAddChar
+
+namespace UnitaryOneParameterGroup
+
+variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
+
+instance : CoeFun (UnitaryOneParameterGroup H) fun _ => ℝ → (H →L[ℂ] H) :=
+  ⟨fun U t => U.toAddChar t⟩
+
+/-- The operator-valued additive character underlying a unitary one-parameter group. -/
+def operatorAddChar (U : UnitaryOneParameterGroup H) : AddChar ℝ (H →L[ℂ] H) :=
+  (unitary (H →L[ℂ] H)).subtype.compAddChar U.toAddChar
+
+@[simp]
+lemma operatorAddChar_apply (U : UnitaryOneParameterGroup H) (t : ℝ) :
+    U.operatorAddChar t = U t := rfl
+
+lemma continuous_operatorAddChar (U : UnitaryOneParameterGroup H) :
+    Continuous U.operatorAddChar :=
+  continuous_subtype_val.comp U.continuous
+
+@[ext]
+lemma ext {U V : UnitaryOneParameterGroup H} (h : ∀ t, U t = V t) : U = V := by
+  cases U
+  cases V
+  congr
+  exact AddChar.ext _ _ fun t => Subtype.ext (h t)
+
+@[simp]
+lemma adjoint_eq (U : UnitaryOneParameterGroup H) (t : ℝ) :
+    ContinuousLinearMap.adjoint (U t) = U (-t) := by
+  change star (U t) = U (-t)
+  apply left_inv_eq_right_inv (U.toAddChar t).property.1
+  have h := congrArg Subtype.val (U.toAddChar.map_add_eq_mul t (-t))
+  simpa using h.symm
+
+/-- The bounded self-adjoint generator of `U`, in the convention `U(t) = exp (-itA)`. -/
+noncomputable def generator (U : UnitaryOneParameterGroup H) : H →L[ℂ] H :=
+  Complex.I • deriv U.operatorAddChar 0
+
+lemma deriv_star_eq_neg (U : UnitaryOneParameterGroup H) :
+    star (deriv U.operatorAddChar 0) = -deriv U.operatorAddChar 0 := by
+  let A : H →L[ℂ] H := deriv U.operatorAddChar 0
+  have hA (t : ℝ) : U t = NormedSpace.exp ((t : ℂ) • A) := by
+    change U.operatorAddChar t = _
+    dsimp only [A]
+    simpa only [Complex.coe_smul] using
+      OneParameterSubgroup.apply_eq_exp_smul_deriv U.operatorAddChar
+        U.continuous_operatorAddChar t
+  have hrep : ∀ t : ℝ, U.operatorAddChar t =
+      NormedSpace.exp ((t : ℂ) • (-star A)) := by
+    intro t
+    calc
+      U.operatorAddChar t = star (U (-t)) := by
+        change U t = ContinuousLinearMap.adjoint (U (-t))
+        simpa only [neg_neg] using (U.adjoint_eq (-t)).symm
+      _ = star (NormedSpace.exp (((-t : ℝ) : ℂ) • A)) := by rw [hA (-t)]
+      _ = NormedSpace.exp (star (((-t : ℝ) : ℂ) • A)) := NormedSpace.star_exp _
+      _ = NormedSpace.exp ((t : ℂ) • (-star A)) := by
+        congr 1
+        simp [star_smul]
+  have hgen : -star A = A :=
+    OneParameterSubgroup.generator_unique U.operatorAddChar (-star A) fun t => by
+      simpa only [Complex.coe_smul] using hrep t
+  simpa [A] using congrArg Neg.neg hgen
+
+/-- The generator of a unitary one-parameter group is self-adjoint. -/
+lemma generator_selfAdjoint (U : UnitaryOneParameterGroup H) : IsSelfAdjoint U.generator := by
+  apply IsSelfAdjoint.I_smul_of_mem_skewAdjoint
+  rw [skewAdjoint.mem_iff, U.deriv_star_eq_neg]
+
+/-- A unitary one-parameter group is the exponential of its self-adjoint generator. -/
+lemma apply_eq_exp_generator (U : UnitaryOneParameterGroup H) (t : ℝ) :
+    U t = NormedSpace.exp ((-(t : ℂ) * Complex.I) • U.generator) := by
+  change U.operatorAddChar t = _
+  rw [OneParameterSubgroup.apply_eq_exp_smul_deriv U.operatorAddChar
+    U.continuous_operatorAddChar]
+  apply congrArg NormedSpace.exp
+  rw [generator, smul_smul]
+  apply congrArg (fun z : ℂ => z • deriv U.operatorAddChar 0)
+  rw [mul_assoc, Complex.I_mul_I]
+  simp
+
+/-- An operator representing `U` as `exp (-itA)` is its generator. -/
+lemma generator_unique (U : UnitaryOneParameterGroup H) (A : H →L[ℂ] H)
+    (h : ∀ t : ℝ, U t = NormedSpace.exp ((-(t : ℂ) * Complex.I) • A)) :
+    A = U.generator := by
+  have hrep : ∀ t : ℝ, U.operatorAddChar t =
+      NormedSpace.exp (t • ((-Complex.I) • A)) := by
+    intro t
+    change U t = _
+    rw [h t]
+    congr 1
+    rw [← Complex.coe_smul, smul_smul]
+    apply congrArg (fun z : ℂ => z • A)
+    ring
+  have hderiv : (-Complex.I) • A = deriv U.operatorAddChar 0 :=
+    OneParameterSubgroup.generator_unique U.operatorAddChar ((-Complex.I) • A) hrep
+  calc
+    A = Complex.I • ((-Complex.I) • A) := by rw [smul_smul]; simp
+    _ = Complex.I • deriv U.operatorAddChar 0 := by rw [hderiv]
+    _ = U.generator := rfl
+
+/-- The unitary one-parameter group generated by a bounded self-adjoint operator. -/
+def ofSelfAdjoint {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) :
+    UnitaryOneParameterGroup H := by
+  letI : NormedAlgebra ℚ (H →L[ℂ] H) := .restrictScalars ℚ ℂ (H →L[ℂ] H)
+  let B : H →L[ℂ] H := (-Complex.I) • A
+  have hB : star B = -B := by
+    dsimp [B]
+    rw [star_smul, Complex.star_def, map_neg, Complex.conj_I, hA.star_eq]
+    module
+  let U : AddChar ℝ (unitary (H →L[ℂ] H)) := {
+    toFun t := ⟨NormedSpace.exp ((t : ℂ) • B), by
+      apply NormedSpace.exp_mem_unitary_of_mem_skewAdjoint
+      rw [skewAdjoint.mem_iff, star_smul, Complex.star_def, Complex.conj_ofReal, hB]
+      module⟩
+    map_zero_eq_one' := by ext; simp
+    map_add_eq_mul' := fun s t => by
+      apply Subtype.ext
+      have hcomm : Commute ((s : ℂ) • B) ((t : ℂ) • B) :=
+        ((Commute.refl B).smul_left _).smul_right _
+      change NormedSpace.exp (((s + t : ℝ) : ℂ) • B) =
+        NormedSpace.exp ((s : ℂ) • B) * NormedSpace.exp ((t : ℂ) • B)
+      rw [← NormedSpace.exp_add_of_commute hcomm]
+      push_cast
+      rw [add_smul] }
+  exact ⟨U, Continuous.subtype_mk (by
+    change Continuous (fun t : ℝ => NormedSpace.exp ((t : ℂ) • B))
+    fun_prop) _⟩
+
+@[simp]
+lemma ofSelfAdjoint_apply {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (t : ℝ) :
+    ofSelfAdjoint hA t = NormedSpace.exp ((-(t : ℂ) * Complex.I) • A) := by
+  simp only [ofSelfAdjoint]
+  change NormedSpace.exp ((t : ℂ) • ((-Complex.I) • A)) = _
+  rw [smul_smul]
+  congr 1
+  ring_nf
+
+/-- Stone's correspondence between norm-continuous unitary one-parameter groups and bounded
+self-adjoint generators. -/
+noncomputable def stoneEquiv :
+    UnitaryOneParameterGroup H ≃ {A : H →L[ℂ] H // IsSelfAdjoint A} where
+  toFun U := ⟨U.generator, U.generator_selfAdjoint⟩
+  invFun A := ofSelfAdjoint A.2
+  left_inv U := by
+    apply ext
+    intro t
+    rw [ofSelfAdjoint_apply, U.apply_eq_exp_generator]
+  right_inv A := by
+    apply Subtype.ext
+    exact ((ofSelfAdjoint A.2).generator_unique A.1 (ofSelfAdjoint_apply A.2)).symm
+
+end UnitaryOneParameterGroup
diff --git a/Physlib/QuantumMechanics/FiniteTarget.lean b/Physlib/QuantumMechanics/FiniteTarget.lean
index 886ed0251..86c87d527 100644
--- a/Physlib/QuantumMechanics/FiniteTarget.lean
+++ b/Physlib/QuantumMechanics/FiniteTarget.lean
@@ -5,16 +5,15 @@ Authors: Joseph Tooby-Smith
 -/
 module
 
-public import Mathlib.Analysis.InnerProductSpace.Adjoint
-public import Mathlib.Analysis.Normed.Algebra.Exponential
+public import Physlib.Mathematics.OneParameterSubgroups.Unitary
 public import Physlib.Meta.TODO.Basic
 public import Physlib.QuantumMechanics.PlanckConstant
 /-!
 
-# Finite target quantum mechanics
+# Finite-dimensional quantum systems
 
-The phrase 'finite target' is used to describe quantum mechanical systems where the
-Hilbert space is finite.
+A `FiniteTarget` consists of a finite-dimensional Hilbert space together with a self-adjoint
+Hamiltonian. Its Hamiltonian determines a unitary time evolution through Stone's correspondence.
 
 Physical examples of such systems include:
 - Spin systems.
@@ -28,42 +27,56 @@ open Constants Module
 
 namespace QuantumMechanics
 
-/-- A `FiniteTarget` structure that is basis independent, i.e. use a linear map for
-  the hamiltonian instead of a matrix."-/
+/-- A finite-dimensional quantum system with a self-adjoint Hamiltonian. -/
 structure FiniteTarget (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
   [CompleteSpace H] [FiniteDimensional ℂ H] (n : ℕ) where
-  /-- the Hilbert space has the provided (finite) dimension. -/
+  /-- The Hilbert space has dimension `n`. -/
   hdim: Module.finrank ℂ H = n
-  /-- The Hamiltonian, written now as a continuous linear map. -/
+  /-- The Hamiltonian. -/
   Ham : H →L[ℂ] H
-  -- The →L[ℂ]s has a Star algebra structure enabling `timeEvolution` definition below.
   /-- The Hamiltonian is self-adjoint. -/
   Ham_selfAdjoint: IsSelfAdjoint Ham
 
 namespace FiniteTarget
 variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
   [FiniteDimensional ℂ H] -- a Hilbert Space with finite dimension
-variable {n : ℕ}(A : FiniteTarget H n)
-
-/-- Given a finite target QM system `A`, the time evolution operator for a `t : ℝ`,
-  `A.timeEvolution t` is defined as `exp(- I t /ℏ * A.Ham)`. Still a map. -/
-noncomputable def timeEvolution (t : ℝ) : H →L[ℂ] H :=
-  NormedSpace.exp (-(Complex.I * t / ℏ) • A.Ham)
-  -- Note that the `H →L[ℂ] H`s make an algebra over 𝕂 := ℂ, so [Algebra 𝕂 𝔸] is satisfied.
-
-/-- The matrix representation of the time evolution operator in a given basis. Given a
-Planck constant `ℏ`, the matrix is a self-adjoint `n × n` matrix describing the timeEvolution. -/
+variable {n : ℕ} (A : FiniteTarget H n)
+
+/-- The unitary time evolution generated by the Hamiltonian of `A`. -/
+noncomputable def unitaryTimeEvolution : UnitaryOneParameterGroup H :=
+  UnitaryOneParameterGroup.ofSelfAdjoint (A := ((ℏ : ℂ)⁻¹) • A.Ham) (by
+    have hℏself : IsSelfAdjoint (ℏ : ℂ) := by
+      rw [isSelfAdjoint_iff, Complex.star_def, Complex.conj_ofReal]
+    exact hℏself.inv₀.smul A.Ham_selfAdjoint)
+
+/-- The generator of time evolution is the Hamiltonian divided by `ℏ`. -/
+@[simp]
+lemma unitaryTimeEvolution_generator :
+    A.unitaryTimeEvolution.generator = ((ℏ : ℂ)⁻¹) • A.Ham := by
+  apply Eq.symm
+  apply UnitaryOneParameterGroup.generator_unique
+  intro t
+  rw [unitaryTimeEvolution, UnitaryOneParameterGroup.ofSelfAdjoint_apply]
+
+/-- The operator implementing the time evolution of `A` at time `t`. -/
+noncomputable def timeEvolution (t : ℝ) : H →L[ℂ] H := A.unitaryTimeEvolution t
+
+@[simp] lemma timeEvolution_eq_exp (t : ℝ) :
+    A.timeEvolution t = NormedSpace.exp ((-(t : ℂ) * Complex.I / ℏ) • A.Ham) := by
+  rw [timeEvolution, UnitaryOneParameterGroup.apply_eq_exp_generator,
+    unitaryTimeEvolution_generator, smul_smul]
+  congr 1
+
+/-- The matrix of the time-evolution operator at time `t` in the basis `b`. -/
 noncomputable def timeEvolutionMatrix (t : ℝ) (b : Basis (Fin n) ℂ H) :
   Matrix (Fin n) (Fin n) ℂ :=
   LinearMap.toMatrix b b (A.timeEvolution t).toLinearMap
-  -- For `LinearMap.toMatrix`, both `M₁`, `M₂` are H.
 
-/-- An instance of timeEvolutionmatrix over the standard basis. -/
+/-- The matrix of the time-evolution operator in a chosen basis indexed by `Fin n`. -/
 noncomputable def timeEvolutionMatrixStandard (t : ℝ) :
   Matrix (Fin n) (Fin n) ℂ :=
-  -- Use the fact that H ≃ ℂ^n to get a basis
-    let b : Basis (Fin n) ℂ H := Module.finBasisOfFinrankEq ℂ H A.hdim
-    (timeEvolutionMatrix A t b)
+  let b : Basis (Fin n) ℂ H := Module.finBasisOfFinrankEq ℂ H A.hdim
+  timeEvolutionMatrix A t b
 
 TODO "Define a smooth structure on `FiniteTarget`."