diff --git a/Physlib/QuantumMechanics/Operators/OneDimension/Momentum.lean b/Physlib/QuantumMechanics/Operators/OneDimension/Momentum.lean
index 3f8781946..a904c0cbc 100644
--- a/Physlib/QuantumMechanics/Operators/OneDimension/Momentum.lean
+++ b/Physlib/QuantumMechanics/Operators/OneDimension/Momentum.lean
@@ -117,11 +117,11 @@ lemma planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded (k :
 
 /-!
 
-## The momentum operator is self adjoint
+## The momentum operator is symmetric
 
 -/
 
-lemma momentumOperatorUnbounded_isSelfAdjoint : momentumOperatorUnbounded.IsSelfAdjoint := by
+lemma momentumOperatorUnbounded_isSymmetric : momentumOperatorUnbounded.IsSymmetric := by
   intro ψ1 ψ2
   have hint : ∀ f g : 𝓢(ℝ, ℂ),
       MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume :=
diff --git a/Physlib/QuantumMechanics/Operators/OneDimension/Parity.lean b/Physlib/QuantumMechanics/Operators/OneDimension/Parity.lean
index 7e0469e19..a1b8b9ba4 100644
--- a/Physlib/QuantumMechanics/Operators/OneDimension/Parity.lean
+++ b/Physlib/QuantumMechanics/Operators/OneDimension/Parity.lean
@@ -93,14 +93,14 @@ lemma parityOperatorSchwartz_parityOperatorSchwartz (ψ : 𝓢(ℝ, ℂ)) :
 
 /-!
 
-## Parity operator is self adjoint
+## Parity operator is symmetric
 
 -/
 
 open InnerProductSpace
 
-lemma parityOperatorUnbounded_isSelfAdjoint :
-    parityOperatorUnbounded.IsSelfAdjoint := by
+lemma parityOperatorUnbounded_isSymmetric :
+    parityOperatorUnbounded.IsSymmetric := by
   intro ψ1 ψ2
   dsimp [parityOperatorUnbounded]
   rw [schwartzIncl_inner, schwartzIncl_inner]
diff --git a/Physlib/QuantumMechanics/Operators/OneDimension/Position.lean b/Physlib/QuantumMechanics/Operators/OneDimension/Position.lean
index 722911046..e028935dc 100644
--- a/Physlib/QuantumMechanics/Operators/OneDimension/Position.lean
+++ b/Physlib/QuantumMechanics/Operators/OneDimension/Position.lean
@@ -93,12 +93,12 @@ lemma positionStates_generalized_eigenvector_positionOperatorUnbounded (x : ℝ)
 
 /-!
 
-## Position operator is self adjoint
+## Position operator is symmetric
 
 -/
 
-lemma positionOperatorUnbounded_isSelfAdjoint :
-    positionOperatorUnbounded.IsSelfAdjoint := by
+lemma positionOperatorUnbounded_isSymmetric :
+    positionOperatorUnbounded.IsSymmetric := by
   intro ψ1 ψ2
   dsimp [positionOperatorUnbounded]
   rw [schwartzIncl_inner, schwartzIncl_inner]
diff --git a/Physlib/QuantumMechanics/Operators/OneDimension/Unbounded.lean b/Physlib/QuantumMechanics/Operators/OneDimension/Unbounded.lean
index 339e6db17..f2f140975 100644
--- a/Physlib/QuantumMechanics/Operators/OneDimension/Unbounded.lean
+++ b/Physlib/QuantumMechanics/Operators/OneDimension/Unbounded.lean
@@ -62,8 +62,12 @@ lemma isGeneralizedEigenvector_ofSelfCLM_iff {Op : S →L[ℂ] S}
 
 open InnerProductSpace
 
-/-- The condition on an unbounded operator to be self-adjoint. -/
-def IsSelfAdjoint : Prop :=
+/-- The condition for an unbounded operator to be *symmetric* (equivalently, formally
+self-adjoint): `⟪U ψ1, ι ψ2⟫ = ⟪ι ψ1, U ψ2⟫` for all `ψ1 ψ2`. This is the Hermitian
+pairing on the underlying space `S`; on its own it does **not** imply genuine
+self-adjointness (`A† = A`, including equality of domains), which for an unbounded
+operator on a proper dense core is strictly stronger. -/
+def IsSymmetric : Prop :=
   ∀ ψ1 ψ2 : S, ⟪U ψ1, ι ψ2⟫_ℂ = ⟪ι ψ1, U ψ2⟫_ℂ
 
 end UnboundedOperator