From b4c0502b5c2c8607afdc8f6e6533522b9ba74147 Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Wed, 18 Feb 2026 21:12:49 +0000 Subject: [PATCH 1/2] chore: remove unused simp lemmas --- .../HarmonicOscillator/ConfigurationSpace.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean index c4c21cb3..1c4a75c2 100644 --- a/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean +++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean @@ -193,13 +193,13 @@ noncomputable def fromRealLM : ℝ →ₗ[ℝ] ConfigurationSpace := noncomputable def toRealCLM : ConfigurationSpace →L[ℝ] ℝ := toRealLM.mkContinuous 1 (by intro x - simp [toRealLM, norm, mul_comm, mul_left_comm, mul_assoc]) + simp [toRealLM, norm, mul_comm]) /-- Continuous linear map embedding a real value into the configuration space. -/ noncomputable def fromRealCLM : ℝ →L[ℝ] ConfigurationSpace := fromRealLM.mkContinuous 1 (by intro x - simp [fromRealLM, norm, mul_comm, mul_left_comm, mul_assoc]) + simp [fromRealLM, norm, mul_comm]) /-- Homeomorphism between configuration space and `ℝ` given by `ConfigurationSpace.val`. -/ noncomputable def valHomeomorphism : ConfigurationSpace ≃ₜ ℝ where From 1e4650f4e9197c303a900fba26da8ca5c7f9fac8 Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Wed, 18 Feb 2026 21:15:28 +0000 Subject: [PATCH 2/2] mul_comm also not needed --- .../HarmonicOscillator/ConfigurationSpace.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean index 1c4a75c2..e6b1a68b 100644 --- a/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean +++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean @@ -193,13 +193,13 @@ noncomputable def fromRealLM : ℝ →ₗ[ℝ] ConfigurationSpace := noncomputable def toRealCLM : ConfigurationSpace →L[ℝ] ℝ := toRealLM.mkContinuous 1 (by intro x - simp [toRealLM, norm, mul_comm]) + simp [toRealLM, norm]) /-- Continuous linear map embedding a real value into the configuration space. -/ noncomputable def fromRealCLM : ℝ →L[ℝ] ConfigurationSpace := fromRealLM.mkContinuous 1 (by intro x - simp [fromRealLM, norm, mul_comm]) + simp [fromRealLM, norm]) /-- Homeomorphism between configuration space and `ℝ` given by `ConfigurationSpace.val`. -/ noncomputable def valHomeomorphism : ConfigurationSpace ≃ₜ ℝ where