feat: Reorganise the Mathematics directory

.github/workflows/build.yml

@@ -112,6 +112,11 @@ jobs:
         if: ${{ !cancelled() && steps.alpha_build.outcome == 'success' }}
         run: env LEAN_ABORT_ON_PANIC=1 lake exe alphaFileImports
 
+      # Only reads import headers, so it does not depend on any build having succeeded.
+      - name: Check ForMathlib imports and uses
+        if: ${{ !cancelled() }}
+        run: env LEAN_ABORT_ON_PANIC=1 lake exe forMathlib_lint
+
       # Runs the occasionally used scripts (TODO_to_yml, stats, informal, make_tag), which
       # import Physlib, QuantumInfo and PhyslibAlpha, so both builds must have succeeded.
       - name: auxiliary script test

AGENTS.md

@@ -55,6 +55,8 @@ When a long proof cannot be split, make sure it contains comments.
 - New physics terms that trip the spell-checker go in `scripts/MetaPrograms/spellingWords.txt`.
 - Check that `lake build` works (run `lake exe cache get` first).
 - Check that `lake exe lint_all` passes.
+- Check that `lake exe forMathlib_lint` passes: files in `Physlib/Mathematics/ForMathlib/` may only
+  import from within that directory, and each must be used outside it.
 - Check `./scripts/lint-style.sh`, but **commit your changes first**; this linter reads committed state.
 - Check that `lake exe auxillary_script_test` passes (needs `Physlib`, `QuantumInfo` and
   `PhyslibAlpha` built).

Physlib.lean

@@ -119,20 +119,25 @@ public import Physlib.Mathematics.Calculus.Gradient
 public import Physlib.Mathematics.Calculus.ParametricIntegration
 public import Physlib.Mathematics.Calculus.Wirtinger.Basic
 public import Physlib.Mathematics.Calculus.Wirtinger.Coordinate
-public import Physlib.Mathematics.ConjModule
-public import Physlib.Mathematics.CrossProduct
-public import Physlib.Mathematics.CrossProductMatrix
-public import Physlib.Mathematics.DataStructures.FourTree.Basic
-public import Physlib.Mathematics.DataStructures.FourTree.UniqueMap
-public import Physlib.Mathematics.DataStructures.Matrix.LieTrace
 public import Physlib.Mathematics.Distribution.Basic
 public import Physlib.Mathematics.Distribution.PowMul
-public import Physlib.Mathematics.FDerivCurry
-public import Physlib.Mathematics.Fin
-public import Physlib.Mathematics.Fin.Involutions
-public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Defs
-public import Physlib.Mathematics.Geometry.Metric.Riemannian.Defs
-public import Physlib.Mathematics.HasTemperateGrowth
+public import Physlib.Mathematics.ForMathlib.DataStructures.Matrix.LieTrace
+public import Physlib.Mathematics.ForMathlib.FDerivCurry
+public import Physlib.Mathematics.ForMathlib.Fin
+public import Physlib.Mathematics.ForMathlib.Fin.Involutions
+public import Physlib.Mathematics.ForMathlib.HasTemperateGrowth
+public import Physlib.Mathematics.ForMathlib.LinearMaps
+public import Physlib.Mathematics.ForMathlib.LinearPMap
+public import Physlib.Mathematics.ForMathlib.List
+public import Physlib.Mathematics.ForMathlib.List.InsertIdx
+public import Physlib.Mathematics.ForMathlib.List.InsertionSort
+public import Physlib.Mathematics.ForMathlib.OneParameterSubgroups.Basic
+public import Physlib.Mathematics.ForMathlib.OneParameterSubgroups.Unitary
+public import Physlib.Mathematics.ForMathlib.OrthogonalMatrix
+public import Physlib.Mathematics.ForMathlib.SchurTriangulation
+public import Physlib.Mathematics.ForMathlib.Trigonometry.SinSq
+public import Physlib.Mathematics.ForMathlib.Trigonometry.Tanh
+public import Physlib.Mathematics.Groups.SO3.Basic
 public import Physlib.Mathematics.InnerProductSpace.Adjoint
 public import Physlib.Mathematics.InnerProductSpace.Basic
 public import Physlib.Mathematics.InnerProductSpace.Calculus
@@ -141,22 +146,11 @@ public import Physlib.Mathematics.InnerProductSpace.Submodule
 public import Physlib.Mathematics.KroneckerDelta.Basic
 public import Physlib.Mathematics.KroneckerDelta.Contraction
 public import Physlib.Mathematics.LeviCivita.Basic
-public import Physlib.Mathematics.LinearMaps
-public import Physlib.Mathematics.LinearPMap
-public import Physlib.Mathematics.List
-public import Physlib.Mathematics.List.InsertIdx
-public import Physlib.Mathematics.List.InsertionSort
-public import Physlib.Mathematics.OneParameterSubgroups.Basic
-public import Physlib.Mathematics.OneParameterSubgroups.Unitary
-public import Physlib.Mathematics.OrthogonalMatrix
-public import Physlib.Mathematics.PiTensorProduct
-public import Physlib.Mathematics.Resolvent
-public import Physlib.Mathematics.SO3.Basic
-public import Physlib.Mathematics.SchurTriangulation
+public import Physlib.Mathematics.Modules.ConjModule
+public import Physlib.Mathematics.Modules.CrossProduct
+public import Physlib.Mathematics.Modules.CrossProductMatrix
 public import Physlib.Mathematics.SpecialFunctions.EllipticIntegral
 public import Physlib.Mathematics.SpecialFunctions.PhysHermite
-public import Physlib.Mathematics.Trigonometry.SinSq
-public import Physlib.Mathematics.Trigonometry.Tanh
 public import Physlib.Mathematics.VariationalCalculus.Basic
 public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv
 public import Physlib.Mathematics.VariationalCalculus.HasVarAdjoint

Physlib/ClassicalMechanics/Pendulum/SimplePendulum/PeriodFormula.lean

@@ -7,7 +7,7 @@ module
 
 public import Physlib.ClassicalMechanics.Pendulum.SimplePendulum.SmallAngle
 public import Physlib.Mathematics.SpecialFunctions.EllipticIntegral
-public import Physlib.Mathematics.Trigonometry.SinSq
+public import Physlib.Mathematics.ForMathlib.Trigonometry.SinSq
 /-!
 
 # The period formula of the simple gravity pendulum

Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean

@@ -6,7 +6,7 @@ Authors: Giuseppe Sorge
 module
 
 public import Physlib.ClassicalMechanics.RigidBody.Basic
-public import Physlib.Mathematics.CrossProduct
+public import Physlib.Mathematics.Modules.CrossProduct
 /-!
 
 # Angular momentum of a rigid body

Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean

@@ -6,7 +6,7 @@ Authors: Giuseppe Sorge
 module
 
 public import Physlib.ClassicalMechanics.RigidBody.Motion
-public import Physlib.Mathematics.CrossProductMatrix
+public import Physlib.Mathematics.Modules.CrossProductMatrix
 /-!
 
 # The angular velocity of a rigid body
@@ -22,8 +22,9 @@ rules for time derivatives of matrices used for this live in
 `Physlib.SpaceAndTime.Time.MatrixDerivatives`.
 
 In three dimensions the skew-symmetric tensor `Ω` is dual to the *angular velocity vector*
-`ω(t) = Ωᵛ` via the hat map (`Physlib.Mathematics.CrossProductMatrix`), with `[ω]ₓ = Ω`; `ω` is the
-angular velocity proper, appearing in the decomposition `v = V + ω × r` as an honest cross product.
+`ω(t) = Ωᵛ` via the hat map (`Physlib.Mathematics.Modules.CrossProductMatrix`), with
+`[ω]ₓ = Ω`; `ω` is the angular velocity proper, appearing in the decomposition `v = V + ω × r`
+as an honest cross product.
 
 The angular velocity can equally be expressed in the *body frame*: the moving coordinate system
 rigidly attached to the body, with origin at the centre of mass and axes rotating with the body,

Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean

@@ -7,7 +7,7 @@ module
 
 public import Physlib.ClassicalMechanics.RigidBody.AngularMomentum
 public import Physlib.ClassicalMechanics.RigidBody.AngularVelocity
-public import Physlib.Mathematics.OrthogonalMatrix
+public import Physlib.Mathematics.ForMathlib.OrthogonalMatrix
 /-!
 
 # Kinetic energy of a rigid body

Physlib/Mathematics/Calculus/AdjFDeriv.lean

@@ -6,7 +6,7 @@ Authors: Tomas Skrivan
 module
 
 public import Mathlib.Analysis.Calculus.Gradient.Basic
-public import Physlib.Mathematics.FDerivCurry
+public import Physlib.Mathematics.ForMathlib.FDerivCurry
 public import Physlib.Mathematics.InnerProductSpace.Adjoint
 public import Physlib.Mathematics.InnerProductSpace.Calculus
 /-!