diff --git a/Physlib/QuantumMechanics/OneDimension/Operators/Position.lean b/Physlib/QuantumMechanics/OneDimension/Operators/Position.lean index d0e8de9a2..3a2e54c1c 100644 --- a/Physlib/QuantumMechanics/OneDimension/Operators/Position.lean +++ b/Physlib/QuantumMechanics/OneDimension/Operators/Position.lean @@ -59,7 +59,7 @@ open ContDiff open SchwartzMap -/-- The parity operator on the Schwartz maps is defined as the linear map from +/-- The position operator on the Schwartz maps is defined as the linear map from `𝓢(ℝ, ℂ)` to itself, such that `ψ` is taken to `fun x => x * ψ x`. -/ def positionOperatorSchwartz : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) := Distribution.powOneMul ℂ