From dc66f1286fbe180e08a2f91f026157b6234676a5 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 3 Jul 2026 13:25:49 +0100 Subject: [PATCH] auto-task(positionOperatorSchwartz): fix doc-string mislabeling it the parity operator Co-authored-by: Claude --- Physlib/QuantumMechanics/OneDimension/Operators/Position.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 ℂ