diff --git a/PhysLean.lean b/PhysLean.lean
index 3d74d9032..67cc5431f 100644
--- a/PhysLean.lean
+++ b/PhysLean.lean
@@ -225,6 +225,10 @@ import PhysLean.QFT.QED.AnomalyCancellation.Odd.Parameterization
 import PhysLean.QFT.QED.AnomalyCancellation.Permutations
 import PhysLean.QFT.QED.AnomalyCancellation.Sorts
 import PhysLean.QFT.QED.AnomalyCancellation.VectorLike
+import PhysLean.QuantumMechanics.DDimensions.Operators.AngularMomentum
+import PhysLean.QuantumMechanics.DDimensions.Operators.Commutation
+import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum
+import PhysLean.QuantumMechanics.DDimensions.Operators.Position
 import PhysLean.QuantumMechanics.FiniteTarget.Basic
 import PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace
 import PhysLean.QuantumMechanics.OneDimension.GeneralPotential.Basic
diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/AngularMomentum.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/AngularMomentum.lean
new file mode 100644
index 000000000..34dfa0f1d
--- /dev/null
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/AngularMomentum.lean
@@ -0,0 +1,120 @@
+/-
+Copyright (c) 2026 Gregory J. Loges. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gregory J. Loges
+-/
+import PhysLean.QuantumMechanics.DDimensions.Operators.Position
+import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum
+/-!
+
+# Angular momentum operator
+
+In this module we define:
+- The angular momentum operator on Schwartz maps, component-wise.
+- The angular momentum squared operator.
+- The angular momentum scalar operator in 2d and angular momentum vector operator in 3d.
+
+-/
+
+namespace QuantumMechanics
+noncomputable section
+open Constants
+open ContDiff SchwartzMap
+
+/-
+
+# Definition
+
+-/
+
+/-- Component `i j` of the angular momentum operator is the continuous linear map
+from `𝓢(Space d, ℂ)` to itself defined by `𝐋ᵢⱼ ≔ 𝐱ᵢ∘𝐩ⱼ - 𝐱ⱼ∘𝐩ᵢ`. -/
+@[sorryful]
+def angularMomentumOperator {d : ℕ} (i j : Fin d) : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
+  𝐱[i] ∘L 𝐩[j] - 𝐱[j] ∘L 𝐩[i]
+
+@[inherit_doc angularMomentumOperator]
+macro "𝐋[" i:term "," j:term "]" : term => `(angularMomentumOperator $i $j)
+
+@[sorryful]
+lemma angularMomentumOperator_apply_fun {d : ℕ} (i j : Fin d) (ψ : 𝓢(Space d, ℂ)) :
+    𝐋[i,j] ψ = 𝐱[i] (𝐩[j] ψ) - 𝐱[j] (𝐩[i] ψ) := rfl
+
+@[sorryful]
+lemma angularMomentumOperator_apply {d : ℕ} (i j : Fin d) (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
+    𝐋[i,j] ψ x = 𝐱[i] (𝐩[j] ψ) x - 𝐱[j] (𝐩[i] ψ) x := rfl
+
+/-- The square of the angular momentum operator, `𝐋² ≔ ½ ∑ᵢⱼ 𝐋ᵢⱼ∘𝐋ᵢⱼ`. -/
+@[sorryful]
+def angularMomentumOperatorSqr {d : ℕ} : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
+  ∑ i, ∑ j, (2 : ℂ)⁻¹ • 𝐋[i,j] ∘L 𝐋[i,j]
+
+@[inherit_doc angularMomentumOperatorSqr]
+notation "𝐋²" => angularMomentumOperatorSqr
+
+@[sorryful]
+lemma angularMomentumOperatorSqr_apply_fun {d : ℕ} (ψ : 𝓢(Space d, ℂ)) :
+    𝐋² ψ = ∑ i, ∑ j, (2 : ℂ)⁻¹ • 𝐋[i,j] (𝐋[i,j] ψ) := by
+  dsimp only [angularMomentumOperatorSqr]
+  simp only [ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_smul',
+    ContinuousLinearMap.coe_comp', Finset.sum_apply, Pi.smul_apply, Function.comp_apply]
+
+@[sorryful]
+lemma angularMomentumOperatorSqr_apply {d : ℕ} (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
+    𝐋² ψ x = ∑ i, ∑ j, (2 : ℂ)⁻¹ * 𝐋[i,j] (𝐋[i,j] ψ) x := by
+  rw [angularMomentumOperatorSqr_apply_fun]
+  rw [← SchwartzMap.coe_coeHom]
+  simp only [map_sum, Finset.sum_apply]
+  rfl
+
+/-
+
+## Basic properties
+
+-/
+
+/-- The angular momentum operator is antisymmetric, `𝐋ᵢⱼ = -𝐋ⱼᵢ` -/
+@[sorryful]
+lemma angularMomentumOperator_antisymm {d : ℕ} (i j : Fin d) : 𝐋[i,j] = - 𝐋[j,i] :=
+  Eq.symm (neg_sub _ _)
+
+/-- Angular momentum operator components with repeated index vanish, `𝐋ᵢᵢ = 0`. -/
+@[sorryful]
+lemma angularMomentumOperator_eq_zero {d : ℕ} (i : Fin d) : 𝐋[i,i] = 0 := sub_self _
+
+/-
+
+## Special cases in low dimensions
+
+  • d = 1 : The angular momentum operator is trivial.
+
+  • d = 2 : The angular momentum operator has only one independent component, 𝐋₀₁, which may
+            be thought of as a (pseudo)scalar operator.
+
+  • d = 3 : The angular momentum operator has three independent components, 𝐋₀₁, 𝐋₁₂ and 𝐋₂₀.
+            Dualizing using the Levi-Civita symbol produces the familiar (pseudo)vector angular
+            momentum operator with components 𝐋₀ = 𝐋₂₀, 𝐋₁ = 𝐋₂₀ and 𝐋₂ = 𝐋₀₁.
+
+-/
+
+/-- In one dimension the angular momentum operator is trivial. -/
+@[sorryful]
+lemma angularMomentumOperator1D_trivial : ∀ (i j : Fin 1), 𝐋[i,j] = 0 := by
+  intro i j
+  fin_cases i, j
+  exact angularMomentumOperator_eq_zero 0
+
+/-- The angular momentum (pseudo)scalar operator in two dimensions, `𝐋 ≔ 𝐋₀₁`. -/
+@[sorryful]
+def angularMomentumOperator2D : 𝓢(Space 2, ℂ) →L[ℂ] 𝓢(Space 2, ℂ) := 𝐋[0,1]
+
+/-- The angular momentum (pseudo)vector operator in three dimension, `𝐋ᵢ ≔ ½ ∑ⱼₖ εᵢⱼₖ 𝐋ⱼₖ`. -/
+@[sorryful]
+def angularMomentumOperator3D (i : Fin 3) : 𝓢(Space 3, ℂ) →L[ℂ] 𝓢(Space 3, ℂ) :=
+  match i with
+    | 0 => 𝐋[1,2]
+    | 1 => 𝐋[2,0]
+    | 2 => 𝐋[0,1]
+
+end
+end QuantumMechanics
diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean
new file mode 100644
index 000000000..295062423
--- /dev/null
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean
@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2026 Gregory J. Loges. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gregory J. Loges
+-/
+import PhysLean.QuantumMechanics.DDimensions.Operators.AngularMomentum
+/-!
+
+# Commutation relations
+
+-/
+
+namespace QuantumMechanics
+noncomputable section
+open Constants
+open SchwartzMap
+
+/-
+## Position / position commutators
+-/
+
+/-- `[xᵢ, xⱼ] = 0` -/
+@[sorryful]
+lemma position_commutation_position {d : ℕ} (i j : Fin d) : ⁅𝐱[i], 𝐱[j]⁆ = 0 := by
+  dsimp only [Bracket.bracket]
+  ext ψ x
+  simp only [ContinuousLinearMap.coe_sub', ContinuousLinearMap.coe_mul, Pi.sub_apply, sub_apply,
+    Function.comp_apply, ContinuousLinearMap.zero_apply, zero_apply, positionOperator_apply]
+  ring
+
+/-
+## Momentum / momentum commutators
+-/
+
+/-- `[pᵢ, pⱼ] = 0` -/
+@[sorryful]
+lemma momentum_commutation_momentum {d : ℕ} (i j : Fin d) : ⁅𝐩[i], 𝐩[j]⁆ = 0 := by
+  sorry
+
+@[sorryful]
+lemma momentum_momentum_eq {d : ℕ} (i j : Fin d) : 𝐩[i] ∘L 𝐩[j] = 𝐩[j] ∘L 𝐩[i] := by
+  rw [← sub_eq_zero]
+  exact momentum_commutation_momentum i j
+
+/-- `[𝐩², 𝐩ᵢ] = 0` -/
+@[sorryful]
+lemma momentumSqr_commutation_momentum {d : ℕ} (i : Fin d) : 𝐩² ∘L 𝐩[i] - 𝐩[i] ∘L 𝐩² = 0 := by
+  dsimp only [momentumOperatorSqr]
+  simp only [ContinuousLinearMap.finset_sum_comp, ContinuousLinearMap.comp_finset_sum]
+  rw [sub_eq_zero]
+  congr
+  ext j ψ x
+  rw [ContinuousLinearMap.comp_assoc]
+  rw [momentum_momentum_eq]
+  rw [← ContinuousLinearMap.comp_assoc]
+  rw [momentum_momentum_eq]
+  rfl
+
+/-
+## Position / momentum commutators
+-/
+
+/-- `[xᵢ, pⱼ] = iℏ δᵢⱼ𝟙` -/
+@[sorryful]
+lemma position_commutation_momentum {d : ℕ} (i j : Fin d) : ⁅𝐱[i], 𝐩[j]⁆ =
+    (Complex.I * ℏ) • (if i = j then 1 else 0) • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ) := by
+  sorry
+
+/-
+## Angular momentum / position commutators
+-/
+
+@[sorryful]
+lemma angularMomentum_commutation_position {d : ℕ} (i j k : Fin d) : ⁅𝐋[i,j], 𝐱[k]⁆ =
+    (Complex.I * ℏ) • ((if i = k then 1 else 0) * 𝐱[j] - (if j = k then 1 else 0) * 𝐱[i]) := by
+  sorry
+
+@[sorryful]
+lemma angularMomentumSqr_commutation_position {d : ℕ} (i : Fin d) :
+    𝐋² ∘L 𝐱[i] - 𝐱[i] ∘L 𝐋² = 0 := by
+  sorry
+
+/-
+## Angular momentum / momentum commutators
+-/
+
+@[sorryful]
+lemma angularMomentum_commutation_momentum {d : ℕ} (i j k : Fin d) : ⁅𝐋[i,j], 𝐩[k]⁆ =
+    (Complex.I * ℏ) • ((if i = k then 1 else 0) * 𝐩[j] - (if j = k then 1 else 0) * 𝐩[i]) := by
+  sorry
+
+/-
+## Angular momentum / angular momentum commutators
+-/
+
+@[sorryful]
+lemma angularMomentum_commutation_angularMomentum {d : ℕ} (i j k l : Fin d) : ⁅𝐋[i,j], 𝐋[k,l]⁆ =
+    (Complex.I * ℏ) • ((if i = k then 1 else 0) * 𝐋[j,l]
+                      - (if i = l then 1 else 0) * 𝐋[j,k]
+                      - (if j = k then 1 else 0) * 𝐋[i,l]
+                      + (if j = l then 1 else 0) * 𝐋[i,k]) := by
+  sorry
+
+@[sorryful]
+lemma angularMomentumSqr_commutation_angularMomentum {d : ℕ} (i j : Fin d) :
+    𝐋² ∘L 𝐋[i,j] - 𝐋[i,j] ∘L 𝐋² = 0 := by
+  sorry
+
+end
+end QuantumMechanics
diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
new file mode 100644
index 000000000..657bec8a4
--- /dev/null
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 Gregory J. Loges. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gregory J. Loges
+-/
+import PhysLean.SpaceAndTime.Space.Derivatives.Basic
+import PhysLean.QuantumMechanics.PlanckConstant
+/-!
+
+# Momentum vector operator
+
+In this module we define:
+- The momentum operator on Schwartz maps, component-wise.
+- The momentum squared operator on Schwartz maps.
+
+-/
+
+namespace QuantumMechanics
+noncomputable section
+open Constants
+open Space
+open ContDiff SchwartzMap
+
+/-- Component `i` of the momentum operator is the continuous linear map
+from `𝓢(Space d, ℂ)` to itself which maps `ψ` to `-iℏ ∂ᵢψ`. -/
+def momentumOperator {d : ℕ} (i : Fin d) : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
+  (- Complex.I * ℏ) • (SchwartzMap.evalCLM (basis i)) ∘L (SchwartzMap.fderivCLM ℂ)
+
+@[inherit_doc momentumOperator]
+macro "𝐩[" i:term "]" : term => `(momentumOperator $i)
+
+lemma momentumOperator_apply_fun {d : ℕ} (i : Fin d) (ψ : 𝓢(Space d, ℂ)) :
+    𝐩[i] ψ = (- Complex.I * ℏ) • ∂[i] ψ := rfl
+
+lemma momentumOperator_apply {d : ℕ} (i : Fin d) (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
+    𝐩[i] ψ x = - Complex.I * ℏ * ∂[i] ψ x := rfl
+
+/-- The square of the momentum operator, `𝐩² ≔ ∑ᵢ 𝐩ᵢ∘𝐩ᵢ`. -/
+def momentumOperatorSqr {d : ℕ} : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) := ∑ i, 𝐩[i] ∘L 𝐩[i]
+
+@[inherit_doc momentumOperatorSqr]
+notation "𝐩²" => momentumOperatorSqr
+
+lemma momentumOperatorSqr_apply {d : ℕ} (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
+    𝐩² ψ x = ∑ i, 𝐩[i] (𝐩[i] ψ) x := by
+  dsimp only [momentumOperatorSqr]
+  rw [← SchwartzMap.coe_coeHom]
+  simp only [ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp', Finset.sum_apply,
+    Function.comp_apply, map_sum]
+
+end
+end QuantumMechanics
diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Position.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Position.lean
new file mode 100644
index 000000000..1bb54147d
--- /dev/null
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Position.lean
@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2026 Gregory J. Loges. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gregory J. Loges
+-/
+import PhysLean.SpaceAndTime.Space.Derivatives.Basic
+/-!
+
+# Position vector operator
+
+In this module we define:
+- The position operator on Schwartz maps, component-wise.
+
+-/
+
+namespace QuantumMechanics
+noncomputable section
+open Space
+open ContDiff SchwartzMap
+
+/-- Component `i` of the position operator is the continuous linear map
+from `𝓢(Space d, ℂ)` to itself which maps `ψ` to `xᵢψ`. -/
+@[sorryful]
+def positionOperator {d : ℕ} (i : Fin d) : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) := by
+  refine SchwartzMap.mkCLM (fun ψ x ↦ x i * ψ x) ?hadd ?hsmul ?hsmooth ?hbound
+  -- hadd
+  · intro ψ1 ψ2 x
+    simp only [SchwartzMap.add_apply]
+    ring
+
+  -- hsmul
+  · intro c ψ x
+    simp only [SchwartzMap.smul_apply, smul_eq_mul, RingHom.id_apply]
+    ring
+
+  -- hsmooth
+  · intro ψ
+    exact ContDiff.smul (eval_contDiff i) (smooth ψ ⊤)
+
+  -- hbound
+  · intro (k, n)
+    use {(k, n - 1), (k + 1, n)}
+    use n + 1
+    refine ⟨by linarith, ?_⟩
+    intro ψ x
+    simp only [Finset.sup_insert, schwartzSeminormFamily_apply, Finset.sup_singleton,
+      Seminorm.coe_sup, Pi.sup_apply]
+
+    trans ‖x‖ ^ k * ∑ j ∈ Finset.range (n + 1), (n.choose j)
+      * ‖iteratedFDeriv ℝ j (fun x ↦ (x i : ℂ)) x‖
+      * ‖iteratedFDeriv ℝ (n - j) ψ x‖
+    · apply (mul_le_mul_of_nonneg_left ?_ (pow_nonneg (norm_nonneg x) k))
+
+      have hcd : ContDiff ℝ ∞ (fun (x : Space d) ↦ (x i : ℂ)) := by
+        apply ContDiff.fun_comp
+        · change ContDiff ℝ ∞ RCLike.ofRealCLM
+          fun_prop
+        · fun_prop
+      apply norm_iteratedFDeriv_mul_le (N := ∞) hcd (SchwartzMap.smooth ψ ⊤) x ENat.LEInfty.out
+
+    -- h0, h1 and hj are the analogues of `norm_iteratedFDeriv_ofRealCLM ℂ j`
+    -- but including a projection to the i-th component of x
+    have h0 : ‖iteratedFDeriv ℝ 0 (fun x ↦ (x i : ℂ)) x‖ = ‖x i‖ := by
+      simp only [norm_iteratedFDeriv_zero, Complex.norm_real, Real.norm_eq_abs]
+
+    have h1 : ‖iteratedFDeriv ℝ 1 (fun x ↦ (x i : ℂ)) x‖ = 1 := by
+      rw [← norm_iteratedFDeriv_fderiv, norm_iteratedFDeriv_zero]
+      sorry
+
+    have hj : ∀ (j : ℕ), ‖iteratedFDeriv ℝ (j + 2) (fun x ↦ (x i : ℂ)) x‖ = 0 := by
+      intro j
+      rw [← norm_iteratedFDeriv_fderiv, ← norm_iteratedFDeriv_fderiv]
+      sorry
+
+    have hproj : ∀ (j : ℕ), ‖iteratedFDeriv ℝ j (fun x ↦ (x i : ℂ)) x‖ =
+        if j = 0 then ‖x i‖ else if j = 1 then 1 else 0 := by
+      intro j
+      match j with
+        | 0 => rw [h0]; simp
+        | 1 => rw [h1]; simp
+        | k + 2 => rw [hj]; simp
+
+    conv_lhs =>
+      enter [2, 2, j, 1, 2]
+      rw [hproj]
+
+    match n with
+      | 0 =>
+        simp only [zero_add, Finset.range_one, Real.norm_eq_abs, mul_ite, mul_one, mul_zero,
+          ite_mul, zero_mul, Finset.sum_singleton, ↓reduceIte, Nat.choose_self, Nat.cast_one,
+          one_mul, Nat.sub_zero, norm_iteratedFDeriv_zero, CharP.cast_eq_zero]
+        trans (SchwartzMap.seminorm ℝ (k + 1) 0) ψ
+        · apply le_trans ?_ (ψ.le_seminorm _ _ _ x)
+          rw [norm_iteratedFDeriv_zero, ← mul_assoc, pow_add]
+          apply (mul_le_mul_of_nonneg_right ?_ (norm_nonneg (ψ x)))
+          apply (mul_le_mul_of_nonneg_left ?_ ?_)
+          · simp only [pow_one, abs_eval_le_norm]
+          · apply pow_nonneg (norm_nonneg _)
+        · exact le_max_right _ _
+      | .succ n =>
+        rw [Finset.sum_range_succ', Finset.sum_range_succ']
+        simp only [Nat.succ_eq_add_one, Nat.add_eq_zero_iff, one_ne_zero, and_false, and_self,
+          ↓reduceIte, Nat.add_eq_right, mul_zero, zero_mul, Finset.sum_const_zero, zero_add,
+          Nat.choose_one_right, Nat.cast_add, Nat.cast_one, mul_one, Nat.reduceAdd,
+          Nat.add_one_sub_one, Nat.choose_zero_right, Real.norm_eq_abs, one_mul, Nat.sub_zero,
+          add_tsub_cancel_right, ge_iff_le]
+
+        trans (↑n + 1) * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n ψ x‖)
+          + (‖x‖ ^ k * |x i| * ‖iteratedFDeriv ℝ (n + 1) ψ x‖)
+        · apply le_of_eq
+          ring
+
+        trans (↑n + 1) * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n ψ x‖)
+          + (‖x‖ ^ (k + 1) * ‖iteratedFDeriv ℝ (n + 1) ψ x‖)
+        · apply add_le_add_right
+          apply mul_le_mul_of_nonneg_right
+          · rw [pow_add, pow_one]
+            apply mul_le_mul_of_nonneg_left
+            · exact abs_eval_le_norm x i
+            · exact pow_nonneg (norm_nonneg x) k
+          · exact ContinuousMultilinearMap.opNorm_nonneg _
+
+        trans (↑n + 1) * (SchwartzMap.seminorm ℂ k (n) ψ)
+          + (SchwartzMap.seminorm ℂ (k + 1) (n + 1) ψ)
+        · apply add_le_add _ (ψ.le_seminorm _ _ _ _)
+          apply mul_le_mul_of_nonneg_left (ψ.le_seminorm _ _ _ _)
+          exact Left.add_nonneg (Nat.cast_nonneg' n) (zero_le_one' ℝ)
+
+        by_cases h : (SchwartzMap.seminorm ℂ (k + 1) (n + 1)) ψ < (SchwartzMap.seminorm ℂ k n) ψ
+        · rw [max_eq_left_of_lt h]
+          trans (↑n + 1) * (SchwartzMap.seminorm ℂ k n) ψ + (SchwartzMap.seminorm ℂ k n) ψ
+          · apply (add_le_add (by linarith) (le_of_lt h))
+          apply le_of_eq
+          ring
+        · rw [not_lt] at h
+          rw [max_eq_right h]
+          trans (↑n + 1) * (SchwartzMap.seminorm ℂ (k + 1) (n + 1)) ψ
+            + (SchwartzMap.seminorm ℂ (k + 1) (n + 1)) ψ
+          · apply (add_le_add ?_ (Std.IsPreorder.le_refl _))
+            apply mul_le_mul_of_nonneg_left h
+            linarith
+          apply le_of_eq
+          ring
+
+@[inherit_doc positionOperator]
+macro "𝐱[" i:term "]" : term => `(positionOperator $i)
+
+@[sorryful]
+lemma positionOperator_apply_fun {d : ℕ} (i : Fin d) (ψ : 𝓢(Space d, ℂ)) :
+    𝐱[i] ψ = (fun x ↦ x i * ψ x) := rfl
+
+@[sorryful]
+lemma positionOperator_apply {d : ℕ} (i : Fin d) (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
+    𝐱[i] ψ x = x i * ψ x := rfl
+
+end
+end QuantumMechanics