leanprover-community · zhikaip · Sep 30, 2026 · Sep 29, 2026 · Sep 29, 2026 · Sep 30, 2026
diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean
@@ -6,8 +6,7 @@ Authors: Nicola Bernini, Nathaneal Sajan
 module
 
 public import Physlib.SpaceAndTime.Space.Basic
-public import Mathlib.Geometry.Manifold.Diffeomorph
-public import Mathlib.Geometry.Manifold.VectorBundle.Tangent
+public import Physlib.Meta.TODO.Basic
 
 /-!
 # Configuration space of the harmonic oscillator

diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Trajectory.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Trajectory.lean
@@ -7,8 +7,6 @@ module
 
 public import Physlib.ClassicalMechanics.HarmonicOscillator.Geometric.Basic
 public import Physlib.SpaceAndTime.Time.Derivatives
-public import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
-public import Mathlib.Geometry.Manifold.MFDeriv.Basic
 /-!
 # Geometric trajectories of the harmonic oscillator
 

diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean
@@ -6,7 +6,6 @@ Authors: Nathaneal Sajan, Joseph Tooby-Smith, Lode Vermeulen
 module
 
 public import Physlib.ClassicalMechanics.HarmonicOscillator.Basic
-public import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 /-!
 
 # Solutions to the classical harmonic oscillator

diff --git a/Physlib/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean b/Physlib/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean
@@ -5,11 +5,6 @@ Authors: Rein Zustand
 -/
 module
 
-public import Physlib.Mathematics.InnerProductSpace.Basic
-public import Mathlib.Analysis.InnerProductSpace.Dual
-public import Physlib.SpaceAndTime.Time.Derivatives
-public import Mathlib.Analysis.Calculus.ContDiff.CPolynomial
-public import Physlib.Mathematics.VariationalCalculus.HasVarGradient
 public import Physlib.ClassicalMechanics.EulerLagrange
 
 /-!

diff --git a/Physlib/ClassicalMechanics/Mass/MassUnit.lean b/Physlib/ClassicalMechanics/Mass/MassUnit.lean
@@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Physlib.Units.PositiveRealUnit
-public import Mathlib.Analysis.RCLike.Basic
 /-!
 
 # Units on Mass

diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Basic.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Basic.lean
@@ -8,7 +8,6 @@ module
 public import Physlib.SpaceAndTime.Space.Module
 public import Mathlib.Analysis.SpecialFunctions.Complex.Circle
 public import Mathlib.Geometry.Manifold.Instances.Sphere
-public import Mathlib.Topology.Covering.AddCircle
 /-!
 
 # Configuration space of the simple pendulum

diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Trajectory.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Trajectory.lean
@@ -7,7 +7,6 @@ module
 
 public import Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Geometric.Basic
 public import Physlib.SpaceAndTime.Time.InnerProductSpace
-public import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
 /-!
 
 # Geometric trajectories of the simple pendulum

diff --git a/Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean b/Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean
@@ -7,7 +7,6 @@ module
 
 public import Physlib.ClassicalMechanics.RigidBody.Motion
 public import Physlib.Mathematics.CrossProductMatrix
-public import Physlib.SpaceAndTime.Time.MatrixDerivatives
 /-!
 
 # The angular velocity of a rigid body

diff --git a/Physlib/ClassicalMechanics/RigidBody/Basic.lean b/Physlib/ClassicalMechanics/RigidBody/Basic.lean
@@ -8,6 +8,7 @@ module
 public import Physlib.SpaceAndTime.Space.SmoothFunctions
 public import Physlib.Meta.Informal.Basic
 public import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
+public import Physlib.Meta.TODO.Basic
 /-!
 
 # Rigid bodies

diff --git a/Physlib/ClassicalMechanics/RigidBody/Motion.lean b/Physlib/ClassicalMechanics/RigidBody/Motion.lean
@@ -6,9 +6,7 @@ Authors: Giuseppe Sorge
 module
 
 public import Physlib.ClassicalMechanics.RigidBody.Basic
-public import Physlib.SpaceAndTime.Time.Derivatives
 public import Physlib.SpaceAndTime.Time.MatrixDerivatives
-public import Mathlib.LinearAlgebra.UnitaryGroup
 /-!
 
 # Rigid body motion

diff --git a/Physlib/ClassicalMechanics/RigidBody/SolidSphere.lean b/Physlib/ClassicalMechanics/RigidBody/SolidSphere.lean
@@ -6,8 +6,8 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Physlib.ClassicalMechanics.RigidBody.Basic
-public import Physlib.SpaceAndTime.Space.Integrals.Basic
 public import Physlib.Meta.Linters.Sorry
+public import Mathlib.MeasureTheory.Measure.Haar.Unique
 /-!
 
 # The solid sphere as a rigid body

diff --git a/Physlib/Cosmology/FLRW/Basic.lean b/Physlib/Cosmology/FLRW/Basic.lean
@@ -7,7 +7,6 @@ module
 
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
 public import Physlib.Meta.Linters.Sorry
-public import Physlib.Meta.Informal.Basic
 public import Physlib.Meta.TODO.Basic
 public import Physlib.SpaceAndTime.Time.Derivatives
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean
@@ -5,7 +5,6 @@ Authors: Philippe Kevorkian, Jinzheng Li
 -/
 module
 
-public import Physlib.Meta.TODO.Basic
 public import Physlib.Cosmology.FLRW.Basic
 public import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
 /-!

diff --git a/Physlib/Electromagnetism/Charge/ChargeUnit.lean b/Physlib/Electromagnetism/Charge/ChargeUnit.lean
@@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Physlib.Units.PositiveRealUnit
-public import Mathlib.Analysis.RCLike.Basic
 /-!
 
 # The units of charge

diff --git a/Physlib/Electromagnetism/Distributional/Basic.lean b/Physlib/Electromagnetism/Distributional/Basic.lean
@@ -6,8 +6,6 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Physlib.SpaceAndTime.TimeAndSpace.ConstantTimeDist
-public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv
-public import Physlib.SpaceAndTime.Space.DistOfFunction
 public import Physlib.SpaceAndTime.SpaceTime.TimeSlice
 
 /-!

diff --git a/Physlib/Electromagnetism/Distributional/Dynamics/KineticTerm.lean b/Physlib/Electromagnetism/Distributional/Dynamics/KineticTerm.lean
@@ -7,7 +7,7 @@ module
 
 public import Physlib.Electromagnetism.Distributional.MagneticField
 public import Physlib.Electromagnetism.Dynamics.Basic
-public import Physlib.Mathematics.VariationalCalculus.HasVarGradient
+public import Physlib.Electromagnetism.Distributional.ElectricField
 /-!
 
 # The kinetic term

diff --git a/Physlib/Electromagnetism/Distributional/Dynamics/Lagrangian.lean b/Physlib/Electromagnetism/Distributional/Dynamics/Lagrangian.lean
@@ -7,7 +7,6 @@ module
 
 public import Physlib.Electromagnetism.Distributional.Dynamics.CurrentDensity
 public import Physlib.Electromagnetism.Distributional.Dynamics.KineticTerm
-public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct
 /-!
 
 # The Lagrangian in electromagnetism

diff --git a/Physlib/Electromagnetism/Distributional/ElectricField.lean b/Physlib/Electromagnetism/Distributional/ElectricField.lean
@@ -8,7 +8,6 @@ module
 public import Physlib.Electromagnetism.Distributional.VectorPotential
 public import Physlib.Electromagnetism.Distributional.ScalarPotential
 public import Physlib.Electromagnetism.Distributional.FieldStrength
-public import Physlib.Electromagnetism.Basic
 /-!
 
 # The Electric Field

diff --git a/Physlib/Electromagnetism/Distributional/FieldStrength.lean b/Physlib/Electromagnetism/Distributional/FieldStrength.lean
@@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Physlib.Electromagnetism.Distributional.Basic
-public import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic
 public import Mathlib.Algebra.Order.Archimedean.Real.Hom
 /-!
 

diff --git a/Physlib/Electromagnetism/Distributional/MagneticField.lean b/Physlib/Electromagnetism/Distributional/MagneticField.lean
@@ -5,7 +5,8 @@ Authors: Joseph Tooby-Smith
 -/
 module
 
-public import Physlib.Electromagnetism.Distributional.ElectricField
+public import Physlib.Electromagnetism.Distributional.FieldStrength
+public import Physlib.Electromagnetism.Distributional.VectorPotential
 /-!
 
 # The Magnetic Field

diff --git a/Physlib/Electromagnetism/Dynamics/Lagrangian.lean b/Physlib/Electromagnetism/Dynamics/Lagrangian.lean
@@ -7,7 +7,6 @@ module
 
 public import Physlib.Electromagnetism.Dynamics.CurrentDensity
 public import Physlib.Electromagnetism.Dynamics.KineticTerm
-public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct
 /-!
 
 # The Lagrangian in electromagnetism

diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -6,8 +6,6 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Physlib.Electromagnetism.Kinematics.EMPotential
-public import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic
-public import Mathlib.Algebra.Order.Archimedean.Real.Hom
 /-!
 
 # The Field Strength Tensor

diff --git a/Physlib/Electromagnetism/Kinematics/VectorPotential.lean b/Physlib/Electromagnetism/Kinematics/VectorPotential.lean
@@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Physlib.Electromagnetism.Kinematics.EMPotential
-public import Mathlib.Algebra.Order.Archimedean.Real.Hom
 /-!
 
 # The vector Potential

diff --git a/Physlib/FluidDynamics/Basic.lean b/Physlib/FluidDynamics/Basic.lean
@@ -6,7 +6,7 @@ Authors: Florian Wiesner
 module
 
 public import Physlib.SpaceAndTime.Space.Basic
-public import Physlib.SpaceAndTime.Time.InnerProductSpace
+public import Physlib.SpaceAndTime.Time.Basic
 /-!
 
 # Basic field types for fluid dynamics

diff --git a/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Bernoulli.lean b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Bernoulli.lean
@@ -5,7 +5,6 @@ Authors: Florian Wiesner, Michał Mogielnicki
 -/
 module
 
-public import Physlib.FluidDynamics.CauchyFlow.BodyForce
 public import Physlib.FluidDynamics.FluidFlow.Kinematics
 public import Physlib.FluidDynamics.ThermodynamicCauchyFlow.Basic
 /-!

diff --git a/Physlib/Mathematics/Calculus/Wirtinger/Coordinate.lean b/Physlib/Mathematics/Calculus/Wirtinger/Coordinate.lean
@@ -6,10 +6,7 @@ Authors: Andrea Pari
 module
 
 public import Physlib.Mathematics.Calculus.Wirtinger.Basic
-public import Mathlib.Analysis.Calculus.FDeriv.Pi
-public import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
 public import Mathlib.Analysis.Calculus.FDeriv.Star
-public import Mathlib.Data.Fintype.Defs
 
 /-!
 

diff --git a/Physlib/Mathematics/ConjModule.lean b/Physlib/Mathematics/ConjModule.lean
@@ -5,10 +5,8 @@ Authors: Andrea Pari
 -/
 module
 
-public import Mathlib.Algebra.Module.Equiv.Defs
-public import Mathlib.Algebra.Star.Module
 public import Mathlib.LinearAlgebra.Basis.Defs
-public import Mathlib.Tactic.Ring
+public import Mathlib.Algebra.Star.Basic
 
 /-!
 

diff --git a/Physlib/Mathematics/CrossProduct.lean b/Physlib/Mathematics/CrossProduct.lean
@@ -6,8 +6,6 @@ Authors: Giuseppe Sorge
 module
 
 public import Mathlib.Analysis.Calculus.ContDiff.Operations
-public import Mathlib.Data.Matrix.Mul
-public import Mathlib.Basic.Real.Basic
 public import Mathlib.LinearAlgebra.CrossProduct
 /-!
 

diff --git a/Physlib/Mathematics/CrossProductMatrix.lean b/Physlib/Mathematics/CrossProductMatrix.lean
@@ -5,10 +5,8 @@ Authors: Giuseppe Sorge
 -/
 module
 
-public import Mathlib.Data.Matrix.Mul
 public import Mathlib.Basic.Real.Basic
 public import Mathlib.LinearAlgebra.CrossProduct
-public import Mathlib.LinearAlgebra.Matrix.Notation
 /-!
 
 # The hat map on three-dimensional vectors

diff --git a/Physlib/Mathematics/Fin.lean b/Physlib/Mathematics/Fin.lean
@@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Mathlib.Algebra.Order.Group.Nat
-public import Mathlib.Algebra.Order.Monoid.NatCast
 public import Mathlib.Logic.Equiv.Fin.Basic
 /-!
 # Fin lemmas

diff --git a/Physlib/Mathematics/KroneckerDelta/Basic.lean b/Physlib/Mathematics/KroneckerDelta/Basic.lean
@@ -5,10 +5,6 @@ Authors: Gregory J. Loges
 -/
 module
 
-public import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
-public import Mathlib.Algebra.CharZero.Defs
-public import Mathlib.Algebra.Field.Defs
-public import Mathlib.Algebra.Module.Defs
 public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
 /-!
 

diff --git a/Physlib/Mathematics/LeviCivita/Basic.lean b/Physlib/Mathematics/LeviCivita/Basic.lean
@@ -7,7 +7,6 @@ module
 
 public import Physlib.Mathematics.KroneckerDelta.Basic
 public import Mathlib.LinearAlgebra.Matrix.Permutation
-public import Mathlib.GroupTheory.Perm.Fin
 /-!
 
 # The Levi-Civita symbol in general dimension

diff --git a/Physlib/Mathematics/LinearPMap.lean b/Physlib/Mathematics/LinearPMap.lean
@@ -5,7 +5,7 @@ Authors: Gregory J. Loges
 -/
 module
 
-public import Mathlib.Analysis.InnerProductSpace.LinearPMap
+public import Mathlib.LinearAlgebra.LinearPMap
 /-!
 
 # LinearPMap

diff --git a/Physlib/Mathematics/Resolvent.lean b/Physlib/Mathematics/Resolvent.lean
@@ -6,9 +6,11 @@ Authors: Adam Bornemann
 module
 
 public import Mathlib.Analysis.Calculus.Deriv.Pow
-public import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
 public import Mathlib.Analysis.Distribution.TemperateGrowth
 public import Mathlib.Analysis.Normed.Algebra.GelfandFormula
+public import Mathlib.Analysis.Calculus.ContDiff.Operations
+public import Mathlib.Analysis.Calculus.Deriv.Mul
+public import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
 /-!
 
 # Temperate growth of the resolvent of a non-real complex number

diff --git a/Physlib/Mathematics/VariationalCalculus/Basic.lean b/Physlib/Mathematics/VariationalCalculus/Basic.lean
@@ -6,7 +6,6 @@ Authors: Tomas Skrivan, Joseph Tooby-Smith
 module
 
 public import Physlib.Mathematics.VariationalCalculus.IsTestFunction
-public import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
 /-!
 
 # Fundamental lemma of the calculus of variations

diff --git a/Physlib/Meta/AllFilePaths.lean b/Physlib/Meta/AllFilePaths.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 module
 
-public import Physlib.Meta.TODO.Basic
 /-!
 
 ## Getting an array of all file paths in Physlib.

diff --git a/Physlib/Meta/Informal/Post.lean b/Physlib/Meta/Informal/Post.lean
@@ -7,7 +7,6 @@ module
 
 public import Physlib.Meta.Basic
 public import Physlib.Meta.Informal.Basic
-public import Physlib.Meta.TODO.Basic
 /-!
 
 ## Informal definitions and lemmas

diff --git a/Physlib/Particles/FlavorPhysics/CKMMatrix/Invariants.lean b/Physlib/Particles/FlavorPhysics/CKMMatrix/Invariants.lean
@@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Physlib.Particles.FlavorPhysics.CKMMatrix.Basic
-public import Mathlib.Analysis.Complex.Basic
 /-!
 # Invariants of the CKM Matrix
 

diff --git a/Physlib/Particles/StandardModel/Basic.lean b/Physlib/Particles/StandardModel/Basic.lean
@@ -6,8 +6,8 @@ Authors: Nikolai Kashcheev, Joseph Tooby-Smith
 module
 
 public import Physlib.SpaceAndTime.SpaceTime.Basic
-public import Physlib.Meta.Linters.Sorry
 public import Mathlib.RingTheory.RootsOfUnity.Complex
+public import Physlib.Meta.Informal.Basic
 /-!
 # The Standard Model
 

diff --git a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean
@@ -6,7 +6,7 @@ Authors: Nathaneal Sajan
 module
 
 public import Physlib.Particles.StandardModel.Basic
-public import Physlib.Relativity.Tensors.ComplexTensor.Basic
+public import Physlib.Relativity.Fermions.Weyl.RightHanded
 /-!
 # Down-type singlets
 

diff --git a/Physlib/Particles/StandardModel/Fermions/LeptonDoublet.lean b/Physlib/Particles/StandardModel/Fermions/LeptonDoublet.lean
@@ -6,7 +6,7 @@ Authors: Nathaneal Sajan
 module
 
 public import Physlib.Particles.StandardModel.Basic
-public import Physlib.Relativity.Tensors.ComplexTensor.Basic
+public import Physlib.Relativity.Fermions.Weyl.LeftHanded
 /-!
 # Lepton doublets
 

diff --git a/Physlib/Particles/StandardModel/Fermions/LeptonSinglet.lean b/Physlib/Particles/StandardModel/Fermions/LeptonSinglet.lean
@@ -6,7 +6,7 @@ Authors: Nathaneal Sajan
 module
 
 public import Physlib.Particles.StandardModel.Basic
-public import Physlib.Relativity.Tensors.ComplexTensor.Basic
+public import Physlib.Relativity.Fermions.Weyl.RightHanded
 /-!
 # Charged-lepton singlets
 

diff --git a/Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean b/Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean
@@ -7,9 +7,6 @@ module
 
 public import Physlib.Particles.StandardModel.Basic
 public import Physlib.Relativity.Fermions.Weyl.LeftHanded
-public import Physlib.Relativity.Fermions.Weyl.RightHanded
-public import Physlib.Relativity.Fermions.Weyl.DualLeftHanded
-public import Physlib.Relativity.Fermions.Weyl.DualRightHanded
 /-!
 # The type corresponding to quark doublets
 

diff --git a/Physlib/Particles/StandardModel/Fermions/UpSinglet.lean b/Physlib/Particles/StandardModel/Fermions/UpSinglet.lean
@@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Physlib.Particles.StandardModel.Basic
-public import Physlib.Relativity.Tensors.ComplexTensor.Basic
+public import Physlib.Relativity.Fermions.Weyl.RightHanded
 /-!
 # Up-type singlets
-Original file line number
+Diff line change
@@ Expand Up / @@ -6,7 +6,6 @@ Authors: Nathaneal Sajan, Joseph Tooby-Smith, Lode Vermeulen @@
     module
     public import Physlib.ClassicalMechanics.HarmonicOscillator.Basic
-    public import Mathlib.Analysis.SpecialFunctions.Complex.Arg
     /-!
     # Solutions to the classical harmonic oscillator
@@ Expand Down @@