feat: Update doc

HEPLean · Feb 20, 2025 · 73a3112 · 73a3112
1 parent be10e90
commit 73a3112
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/PhysLean/QuantumMechanics/HarmonicOscillator.lean b/PhysLean/QuantumMechanics/HarmonicOscillator.lean
@@ -23,7 +23,6 @@ This file contains
 
 ## TODO
 - Show that Schrodinger operator is linear.
-- Show that eigenfunctions are orthogonal and normalized.
 - Show that eigenfunctions satisfy the completeness relation.
 
 -/
@@ -514,7 +513,6 @@ lemma eigenFunction_orthogonal (m ℏ ω : ℝ) (n p : ℕ) (hℏ : 0 < ℏ) (hm
   simp
   exact hnp
 
-
 end HarmonicOscillator
 
 end QuantumMechanics