diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean index a4392f4028..a2eec38c39 100644 --- 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 index 4b67ff9e74..0a54431fa9 100644 --- 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 index da7ee06119..56eccde1c1 100644 --- 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 index 356a2561b8..1153d5e766 100644 --- 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 index 7be25d8a9e..e9c805bf20 100644 --- 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 index 1b28933a1a..f255da483a 100644 --- 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 index 722e6c842d..f0fb50647a 100644 --- 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 index 0b3b853996..d8f8dc8a62 100644 --- 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 index 80a5b5539f..2bdb37a1e0 100644 --- 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 index 02daf1fe80..4e2d59232a 100644 --- 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 index f57fd56cc2..203f524ec0 100644 --- 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 index 94baa13f9d..a70b130277 100644 --- 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 index d7edead1d4..ebab8c2fc1 100644 --- 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 index 8b73198190..955a9cb42c 100644 --- 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 index 45c4d48ccf..2364b18651 100644 --- 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 index 5de4e97119..a23453b3a5 100644 --- 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 index c837cf7601..fc65ee9595 100644 --- 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 index e94c954447..91c31c23b7 100644 --- 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 index 3750570786..3a768925d1 100644 --- 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 index 20db7b4e05..9e6e9527ee 100644 --- 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 index e9b5e3a803..8d873ac4d8 100644 --- 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 index 3bb6a84e62..684fa8f630 100644 --- 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 index 04c32604ba..c4b96fccee 100644 --- 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 index 2d7656cbbe..944629af96 100644 --- 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 index 7883b47a61..4a509926d9 100644 --- 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 index 77e67ffdf4..36082e5037 100644 --- 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 index 3b2ce70396..a76b66e6c1 100644 --- 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 index 185aa890c8..10403a7c5d 100644 --- 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 index e48a8c101d..c6f3cb0685 100644 --- 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 index 5aaa564d90..25b6becfe3 100644 --- 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 index 5c639f805b..069948e4fd 100644 --- 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 index d99bd7b42b..788546417f 100644 --- 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 index a35b7df538..56cc1d5eeb 100644 --- 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 index 8141070f6b..c831db20c6 100644 --- 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 index 57c4c57704..251b691ede 100644 --- 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 index 091a737c41..a656a80127 100644 --- 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 index 390b94538e..13af0e1346 100644 --- 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 index 168888bdbe..e6c6628381 100644 --- 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 index 246f77a1d5..cf14aa6b93 100644 --- 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 index 49603c4b4f..f5412abfa5 100644 --- 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 index 050ce49dd3..4350b1f65b 100644 --- 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 index 6a83165aca..426d1b95b1 100644 --- 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 index 43de4ad8c6..010e262d1c 100644 --- 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 index f2b1b1aa04..e0cf04597b 100644 --- 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 diff --git a/Physlib/Particles/StandardModel/HiggsBoson/Potential.lean b/Physlib/Particles/StandardModel/HiggsBoson/Potential.lean index d0dc887898..40444e137a 100644 --- a/Physlib/Particles/StandardModel/HiggsBoson/Potential.lean +++ b/Physlib/Particles/StandardModel/HiggsBoson/Potential.lean @@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith module public import Physlib.Particles.StandardModel.HiggsBoson.Basic -public import Mathlib.RingTheory.MvPolynomial.Homogeneous /-! # The potential of the Higgs field diff --git a/Physlib/Particles/SuperSymmetry/SU5/FieldLabels.lean b/Physlib/Particles/SuperSymmetry/SU5/FieldLabels.lean index 95dc060524..e3411411cf 100644 --- a/Physlib/Particles/SuperSymmetry/SU5/FieldLabels.lean +++ b/Physlib/Particles/SuperSymmetry/SU5/FieldLabels.lean @@ -5,7 +5,8 @@ Authors: Joseph Tooby-Smith -/ module -public import Mathlib.Tactic.DeriveFintype +public import Mathlib.Data.Finset.Insert +public import Mathlib.Data.Fintype.Defs /-! # The field labels diff --git a/Physlib/Particles/SuperSymmetry/SU5/Potential.lean b/Physlib/Particles/SuperSymmetry/SU5/Potential.lean index eaedbe317c..3c03a151c4 100644 --- a/Physlib/Particles/SuperSymmetry/SU5/Potential.lean +++ b/Physlib/Particles/SuperSymmetry/SU5/Potential.lean @@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.Particles.SuperSymmetry.SU5.FieldLabels +public import Mathlib.Tactic.DeriveFintype /-! # Potential of the SU(5) + U(1) GUT diff --git a/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean b/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean index e1940567a6..3f12117061 100644 --- a/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean +++ b/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean @@ -6,8 +6,6 @@ Authors: Tom Ole Diem module public import Mathlib.Analysis.Normed.Module.Basic -public import Mathlib.Topology.Sequences -public import Mathlib.Topology.Order.OrderClosed public import Physlib.ProbabilisticTheory.OrderUnit.Basic /-! diff --git a/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean b/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean index 58d819f703..f6a462a807 100644 --- a/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean +++ b/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean @@ -6,8 +6,6 @@ Authors: Tom Ole Diem module public import Mathlib.Geometry.Convex.Cone.Pointed -public import Mathlib.Basic.Real.Basic -public import Mathlib.Basic.NNReal.Defs public import Physlib.ProbabilisticTheory.OrderUnit.Archimedean /-! diff --git a/Physlib/QFT/PerturbationTheory/FieldStatistics/ExchangeSign.lean b/Physlib/QFT/PerturbationTheory/FieldStatistics/ExchangeSign.lean index 025ffab390..c7bf60ea7c 100644 --- a/Physlib/QFT/PerturbationTheory/FieldStatistics/ExchangeSign.lean +++ b/Physlib/QFT/PerturbationTheory/FieldStatistics/ExchangeSign.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.QFT.PerturbationTheory.FieldStatistics.Basic -public import Mathlib.Analysis.Complex.Basic +public import Mathlib.Basic.Complex.Basic /-! # Exchange sign for field statistics diff --git a/Physlib/QFT/PerturbationTheory/WickAlgebra/Basic.lean b/Physlib/QFT/PerturbationTheory/WickAlgebra/Basic.lean index e9eaf8a61e..3e23848207 100644 --- a/Physlib/QFT/PerturbationTheory/WickAlgebra/Basic.lean +++ b/Physlib/QFT/PerturbationTheory/WickAlgebra/Basic.lean @@ -6,8 +6,6 @@ Authors: Joseph Tooby-Smith module public import Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute -public import Mathlib.Algebra.RingQuot -public import Mathlib.RingTheory.TwoSidedIdeal.Operations /-! # The Wick Algebra diff --git a/Physlib/QFT/PerturbationTheory/WickContraction/ExtractEquiv.lean b/Physlib/QFT/PerturbationTheory/WickContraction/ExtractEquiv.lean index d0cdee2933..ca663d84da 100644 --- a/Physlib/QFT/PerturbationTheory/WickContraction/ExtractEquiv.lean +++ b/Physlib/QFT/PerturbationTheory/WickContraction/ExtractEquiv.lean @@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith -/ module -meta import Physlib.QFT.PerturbationTheory.WickContraction.InsertAndContractNat public import Physlib.QFT.PerturbationTheory.WickContraction.InsertAndContractNat import all Init.Data.Fin.Fold /-! diff --git a/Physlib/QuantumMechanics/Blackbody/PlancksLaw.lean b/Physlib/QuantumMechanics/Blackbody/PlancksLaw.lean index e58e329063..fb3c5c03eb 100644 --- a/Physlib/QuantumMechanics/Blackbody/PlancksLaw.lean +++ b/Physlib/QuantumMechanics/Blackbody/PlancksLaw.lean @@ -5,10 +5,7 @@ Authors: Samyak Rai -/ module -public import Mathlib.Analysis.SpecialFunctions.Exponential -public import Physlib.Meta.Informal.Basic public import Physlib.Thermodynamics.Temperature.Basic -public import Physlib.StatisticalMechanics.BoltzmannConstant public import Physlib.Relativity.SpeedOfLight public import Physlib.QuantumMechanics.PlanckConstant diff --git a/Physlib/QuantumMechanics/FreeParticle/Basic.lean b/Physlib/QuantumMechanics/FreeParticle/Basic.lean index decd44ec99..43679ceb47 100644 --- a/Physlib/QuantumMechanics/FreeParticle/Basic.lean +++ b/Physlib/QuantumMechanics/FreeParticle/Basic.lean @@ -7,7 +7,6 @@ module public import Physlib.Meta.Informal.Basic public import Physlib.QuantumMechanics.Operators.Momentum -public import Physlib.QuantumMechanics.QuantumSystem.Basic /-! # The free particle on `Space d` diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean index 6ed39a58d9..c49053aac6 100644 --- a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean +++ b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean @@ -8,7 +8,6 @@ module public import Physlib.Meta.Informal.Basic public import Physlib.QuantumMechanics.Operators.Momentum public import Physlib.QuantumMechanics.Operators.Multiplication -public import Physlib.QuantumMechanics.QuantumSystem.Basic /-! # The quantum harmonic oscillator diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean index a4cd573d5a..eabb5d2580 100644 --- a/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean +++ b/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean @@ -7,12 +7,9 @@ module public import Physlib.Mathematics.InnerProductSpace.Gaussian public import Physlib.Mathematics.HasTemperateGrowth -public import Physlib.Mathematics.KroneckerDelta.Basic -public import Physlib.Mathematics.SpecialFunctions.PhysHermite -public import Physlib.QuantumMechanics.HarmonicOscillator.Basic public import Physlib.QuantumMechanics.HarmonicOscillator.NumberOperator public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Eigenfunction -public import Physlib.Meta.Sorry +public import Physlib.Meta.Linters.Sorry /-! # Energy eigenstates of the quantum harmonic oscillator diff --git a/Physlib/QuantumMechanics/HilbertSpaces/OneDimension/Gaussians.lean b/Physlib/QuantumMechanics/HilbertSpaces/OneDimension/Gaussians.lean index 382087bd93..e53a74ef77 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/OneDimension/Gaussians.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/OneDimension/Gaussians.lean @@ -7,7 +7,6 @@ module public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.Basic public import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral -public import Physlib.Meta.TODO.Basic /-! # Gaussians and the hilbert space diff --git a/Physlib/QuantumMechanics/HilbertSpaces/OneDimension/SchwartzSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/OneDimension/SchwartzSubmodule.lean index 56d0535252..2a8c9ebae4 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/OneDimension/SchwartzSubmodule.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/OneDimension/SchwartzSubmodule.lean @@ -7,7 +7,6 @@ module public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.Basic public import Mathlib.Analysis.Distribution.SchwartzSpace.Basic -public import Physlib.Meta.TODO.Basic /-! # Schwartz submodule of the Hilbert space diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean index 807c8c5f19..2aaa9101bd 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.Distribution.TemperedDistribution public import Mathlib.Analysis.InnerProductSpace.Dual public import Physlib.SpaceAndTime.Space.Module +public import Physlib.Meta.TODO.Basic /-! # Hilbert spaces for quantum mechanics on `Space d` diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/MomentumStates.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/MomentumStates.lean index 773d7e4d42..0aca64603f 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/MomentumStates.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/MomentumStates.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Distribution.TemperedDistribution public import Physlib.SpaceAndTime.Space.Module +public import Physlib.Meta.TODO.Basic /-! # Momentum states diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean index 5971c08c97..4767a73905 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean @@ -5,7 +5,6 @@ Authors: Gregory J. Loges -/ module -public import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct public import Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmodule /-! diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PositionStates.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PositionStates.lean index a2a61b2d42..b260789734 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PositionStates.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PositionStates.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Distribution.TemperedDistribution public import Physlib.SpaceAndTime.Space.Module +public import Physlib.Meta.TODO.Basic /-! # Position states diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean index e6789f6b43..a79b3fcd44 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean @@ -5,7 +5,6 @@ Authors: Adam Bornemann, Gregory J. Loges -/ module -public import Mathlib.Analysis.Distribution.SchwartzSpace.Basic public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.Basic /-! diff --git a/Physlib/QuantumMechanics/InfiniteSquareWell/Basic.lean b/Physlib/QuantumMechanics/InfiniteSquareWell/Basic.lean index fe3ff960e4..8b7e76f5bf 100644 --- a/Physlib/QuantumMechanics/InfiniteSquareWell/Basic.lean +++ b/Physlib/QuantumMechanics/InfiniteSquareWell/Basic.lean @@ -6,8 +6,7 @@ Authors: Gregory J. Loges module public import Physlib.Meta.Informal.Basic -public import Physlib.QuantumMechanics.Operators.Momentum -public import Physlib.QuantumMechanics.QuantumSystem.Basic +public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.Basic /-! # The infinite square well diff --git a/Physlib/QuantumMechanics/Operators/Commutation.lean b/Physlib/QuantumMechanics/Operators/Commutation.lean index cdad81ca58..eed8c4606c 100644 --- a/Physlib/QuantumMechanics/Operators/Commutation.lean +++ b/Physlib/QuantumMechanics/Operators/Commutation.lean @@ -6,9 +6,9 @@ Authors: Gregory J. Loges module public import Physlib.Mathematics.KroneckerDelta.Basic -public import Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial public import Physlib.QuantumMechanics.Operators.Position public import Physlib.QuantumMechanics.Operators.Momentum +public import Mathlib.Algebra.Lie.OfAssociative /-! # Commutation relations diff --git a/Physlib/QuantumMechanics/Operators/Position.lean b/Physlib/QuantumMechanics/Operators/Position.lean index 49b9d35b02..50aeb65a7f 100644 --- a/Physlib/QuantumMechanics/Operators/Position.lean +++ b/Physlib/QuantumMechanics/Operators/Position.lean @@ -8,6 +8,8 @@ module public import Physlib.QuantumMechanics.Operators.Multiplication public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.PolyBddSchwartzSubmodule public import Physlib.SpaceAndTime.Space.Norm.Regularized +public import Physlib.SpaceAndTime.Space.Derivatives.Basic +public import Physlib.SpaceAndTime.Space.Integrals.NormPow /-! # Position operators diff --git a/Physlib/QuantumMechanics/Operators/StateObservables/IsEigenvector.lean b/Physlib/QuantumMechanics/Operators/StateObservables/IsEigenvector.lean index 04159d7e59..dbf5dc0ffe 100644 --- a/Physlib/QuantumMechanics/Operators/StateObservables/IsEigenvector.lean +++ b/Physlib/QuantumMechanics/Operators/StateObservables/IsEigenvector.lean @@ -5,7 +5,8 @@ Authors: Matteo Cipollina, Krystian Nowakowski -/ module -public import Physlib.QuantumMechanics.Operators.Unbounded +public import Mathlib.Analysis.InnerProductSpace.Defs +public import Mathlib.Analysis.Complex.Basic /-! # Eigenvectors of partial linear maps diff --git a/Physlib/QuantumMechanics/Operators/StateObservables/Variance.lean b/Physlib/QuantumMechanics/Operators/StateObservables/Variance.lean index de9faea890..ce72ab96f1 100644 --- a/Physlib/QuantumMechanics/Operators/StateObservables/Variance.lean +++ b/Physlib/QuantumMechanics/Operators/StateObservables/Variance.lean @@ -7,7 +7,6 @@ module public import Physlib.QuantumMechanics.Operators.StateObservables.ExpectedValue public import Physlib.QuantumMechanics.Operators.StateObservables.IsEigenvector -public import Mathlib.Analysis.SpecialFunctions.Sqrt /-! # Variance and standard deviation diff --git a/Physlib/QuantumMechanics/PlanckConstant.lean b/Physlib/QuantumMechanics/PlanckConstant.lean index 19bd733fb1..025d036a5e 100644 --- a/Physlib/QuantumMechanics/PlanckConstant.lean +++ b/Physlib/QuantumMechanics/PlanckConstant.lean @@ -5,7 +5,6 @@ Authors: Samyak Rai, Joseph Tooby-Smith -/ module -public import Mathlib.Basic.NNReal.Defs public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic /-! diff --git a/Physlib/QuantumMechanics/PoschlTeller/Basic.lean b/Physlib/QuantumMechanics/PoschlTeller/Basic.lean index 175395564d..329894b003 100644 --- a/Physlib/QuantumMechanics/PoschlTeller/Basic.lean +++ b/Physlib/QuantumMechanics/PoschlTeller/Basic.lean @@ -5,11 +5,8 @@ Authors: Afiq Hatta -/ module -public import Physlib.QuantumMechanics.Operators.Momentum -public import Physlib.QuantumMechanics.Operators.Multiplication public import Physlib.QuantumMechanics.SpaceDQuantumSystem public import Physlib.Mathematics.Trigonometry.Tanh -public import Physlib.Meta.TODO.Basic /-! # 1d Pöschl-Teller diff --git a/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean b/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean index 50f9b85838..abed1a2d52 100644 --- a/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean +++ b/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean @@ -8,7 +8,6 @@ module public import Physlib.Meta.Informal.Basic public import Physlib.QuantumMechanics.Operators.Momentum public import Physlib.QuantumMechanics.Operators.Multiplication -public import Physlib.QuantumMechanics.QuantumSystem.Basic /-! # The rectangular potential barrier diff --git a/Physlib/Relativity/Bispinors/Basic.lean b/Physlib/Relativity/Bispinors/Basic.lean index 36a691c05e..e4dc790650 100644 --- a/Physlib/Relativity/Bispinors/Basic.lean +++ b/Physlib/Relativity/Bispinors/Basic.lean @@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.PauliMatrices.ToTensor +public import Physlib.Meta.Informal.Basic /-! ## Bispinors diff --git a/Physlib/Relativity/Fermions/Dirac/Basic.lean b/Physlib/Relativity/Fermions/Dirac/Basic.lean index e92578e2d7..082e364019 100644 --- a/Physlib/Relativity/Fermions/Dirac/Basic.lean +++ b/Physlib/Relativity/Fermions/Dirac/Basic.lean @@ -6,9 +6,8 @@ Authors: Joseph Tooby-Smith module 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 +public import Mathlib.RepresentationTheory.Intertwining /-! # Dirac fermions diff --git a/Physlib/Relativity/Fermions/Dirac/GammaMatrices.lean b/Physlib/Relativity/Fermions/Dirac/GammaMatrices.lean index 758c310d95..b333f5bd15 100644 --- a/Physlib/Relativity/Fermions/Dirac/GammaMatrices.lean +++ b/Physlib/Relativity/Fermions/Dirac/GammaMatrices.lean @@ -6,6 +6,7 @@ Authors: Zhuoran Li module public import Physlib.Relativity.Fermions.Dirac.Basic +public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct /-! # Gamma endomorphisms of Dirac fermions diff --git a/Physlib/Relativity/Fermions/Weyl/Contraction.lean b/Physlib/Relativity/Fermions/Weyl/Contraction.lean index bf2001a743..48a89d65e1 100644 --- a/Physlib/Relativity/Fermions/Weyl/Contraction.lean +++ b/Physlib/Relativity/Fermions/Weyl/Contraction.lean @@ -9,6 +9,7 @@ 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 +public import Mathlib.RepresentationTheory.Intertwining /-! # Contraction of Weyl fermions @@ -32,8 +33,6 @@ open TensorProduct ## Contraction of Weyl fermions. -/ -open CategoryTheory.MonoidalCategory - /-- The bi-linear map corresponding to contraction of a left-handed Weyl fermion with a dual-left-handed Weyl fermion. -/ def leftDualBi : LeftHandedWeyl →ₗ[ℂ] DualLeftHandedWeyl →ₗ[ℂ] ℂ where diff --git a/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean b/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean index a6bc9abe1c..20b631ed94 100644 --- a/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean +++ b/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean @@ -6,10 +6,9 @@ Authors: Joseph Tooby-Smith module public import Mathlib.Analysis.Complex.Basic -public import Physlib.Meta.TODO.Basic -public import Physlib.Relativity.SL2C.Basic -public import Physlib.Meta.Informal.Basic -public import Physlib.Meta.TODO.Basic +public import Mathlib.RepresentationTheory.Basic +public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse +public import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup /-! ## Dual left handed Weyl fermions diff --git a/Physlib/Relativity/Fermions/Weyl/DualRightHanded.lean b/Physlib/Relativity/Fermions/Weyl/DualRightHanded.lean index 1d7fbbeec7..f8df9acf60 100644 --- a/Physlib/Relativity/Fermions/Weyl/DualRightHanded.lean +++ b/Physlib/Relativity/Fermions/Weyl/DualRightHanded.lean @@ -6,10 +6,9 @@ Authors: Joseph Tooby-Smith module public import Mathlib.Analysis.Complex.Basic -public import Physlib.Meta.TODO.Basic -public import Physlib.Relativity.SL2C.Basic -public import Physlib.Meta.Informal.Basic -public import Physlib.Meta.TODO.Basic +public import Mathlib.RepresentationTheory.Basic +public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse +public import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup /-! ## Dual right handed Weyl fermions diff --git a/Physlib/Relativity/Fermions/Weyl/Duals.lean b/Physlib/Relativity/Fermions/Weyl/Duals.lean index 8189a61974..f313c37b07 100644 --- a/Physlib/Relativity/Fermions/Weyl/Duals.lean +++ b/Physlib/Relativity/Fermions/Weyl/Duals.lean @@ -9,6 +9,8 @@ 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 +public import Physlib.Meta.Informal.Basic +public import Physlib.Relativity.SL2C.Basic /-! # Duals for fermions diff --git a/Physlib/Relativity/Fermions/Weyl/LeftHanded.lean b/Physlib/Relativity/Fermions/Weyl/LeftHanded.lean index 45187eaca9..dfcf269ebf 100644 --- a/Physlib/Relativity/Fermions/Weyl/LeftHanded.lean +++ b/Physlib/Relativity/Fermions/Weyl/LeftHanded.lean @@ -6,10 +6,8 @@ Authors: Joseph Tooby-Smith module public import Mathlib.Analysis.Complex.Basic -public import Physlib.Meta.TODO.Basic -public import Physlib.Relativity.SL2C.Basic -public import Physlib.Meta.Informal.Basic -public import Physlib.Meta.TODO.Basic +public import Mathlib.RepresentationTheory.Basic +public import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup /-! ## Left handed Weyl fermions diff --git a/Physlib/Relativity/Fermions/Weyl/RightHanded.lean b/Physlib/Relativity/Fermions/Weyl/RightHanded.lean index 6b68b8c5f5..f145e750a3 100644 --- a/Physlib/Relativity/Fermions/Weyl/RightHanded.lean +++ b/Physlib/Relativity/Fermions/Weyl/RightHanded.lean @@ -6,10 +6,8 @@ Authors: Joseph Tooby-Smith module public import Mathlib.Analysis.Complex.Basic -public import Physlib.Meta.TODO.Basic -public import Physlib.Relativity.SL2C.Basic -public import Physlib.Meta.Informal.Basic -public import Physlib.Meta.TODO.Basic +public import Mathlib.RepresentationTheory.Basic +public import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup /-! ## Right handed Weyl fermions diff --git a/Physlib/Relativity/Fermions/Weyl/Two.lean b/Physlib/Relativity/Fermions/Weyl/Two.lean index 5dd1e72417..36946e3f1d 100644 --- a/Physlib/Relativity/Fermions/Weyl/Two.lean +++ b/Physlib/Relativity/Fermions/Weyl/Two.lean @@ -9,6 +9,7 @@ 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 +public import Physlib.Relativity.SL2C.Basic /-! # Tensor product of two Weyl fermion diff --git a/Physlib/Relativity/LorentzAlgebra/Basic.lean b/Physlib/Relativity/LorentzAlgebra/Basic.lean index 7666e630fe..f2218531f7 100644 --- a/Physlib/Relativity/LorentzAlgebra/Basic.lean +++ b/Physlib/Relativity/LorentzAlgebra/Basic.lean @@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.MinkowskiMatrix -public import Mathlib.Algebra.Lie.SerreConstruction /-! # The Lorentz Algebra diff --git a/Physlib/Relativity/LorentzGroup/Basic.lean b/Physlib/Relativity/LorentzGroup/Basic.lean index ebad7295a2..ebba7a6e19 100644 --- a/Physlib/Relativity/LorentzGroup/Basic.lean +++ b/Physlib/Relativity/LorentzGroup/Basic.lean @@ -7,11 +7,11 @@ module public import Physlib.Relativity.MinkowskiMatrix public import Physlib.Meta.TODO.Basic -public import Mathlib.Analysis.Complex.Basic public import Mathlib.Topology.Instances.Matrix public import Mathlib.Topology.Algebra.Group.Units -public import Mathlib.Topology.Maps.Basic public import Mathlib.Topology.Algebra.Group.ClosedSubgroup +public import Mathlib.Basic.Complex.Basic +public import Mathlib.Topology.Algebra.Ring.Real /-! # The Lorentz Group diff --git a/Physlib/Relativity/LorentzGroup/Boosts/Axis.lean b/Physlib/Relativity/LorentzGroup/Boosts/Axis.lean index d626b69534..eb9a5b9e21 100644 --- a/Physlib/Relativity/LorentzGroup/Boosts/Axis.lean +++ b/Physlib/Relativity/LorentzGroup/Boosts/Axis.lean @@ -6,6 +6,7 @@ Authors: Jinzheng Li, Nathaneal Sajan, Joseph Tooby-Smith module public import Physlib.Relativity.SL2C.AxisRotations +public import Physlib.Relativity.SL2C.Basic /-! # Coordinate-axis boosts in `SL(2,ℂ)` and the Lorentz group diff --git a/Physlib/Relativity/LorentzGroup/Boosts/Basic.lean b/Physlib/Relativity/LorentzGroup/Boosts/Basic.lean index a352a3d82a..71c7c3c8da 100644 --- a/Physlib/Relativity/LorentzGroup/Boosts/Basic.lean +++ b/Physlib/Relativity/LorentzGroup/Boosts/Basic.lean @@ -6,6 +6,8 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.LorentzGroup.Basic +public import Mathlib.Tactic.LinearCombination +public import Mathlib.Analysis.Real.Sqrt /-! # Boosts in the Lorentz group diff --git a/Physlib/Relativity/MinkowskiMatrix.lean b/Physlib/Relativity/MinkowskiMatrix.lean index 001a13b274..d6c59a79a6 100644 --- a/Physlib/Relativity/MinkowskiMatrix.lean +++ b/Physlib/Relativity/MinkowskiMatrix.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith module public import Mathlib.Algebra.Lie.Classical -public import Mathlib.Analysis.Normed.Ring.Lemmas +public import Mathlib.Basic.Real.Basic /-! # The Minkowski matrix diff --git a/Physlib/Relativity/PauliMatrices/Basic.lean b/Physlib/Relativity/PauliMatrices/Basic.lean index 7f2a7c0b63..b80b3e47b9 100644 --- a/Physlib/Relativity/PauliMatrices/Basic.lean +++ b/Physlib/Relativity/PauliMatrices/Basic.lean @@ -8,7 +8,7 @@ module public import Mathlib.Analysis.Complex.Basic public import Mathlib.LinearAlgebra.Matrix.Trace public import Physlib.Mathematics.KroneckerDelta.Basic -public import Physlib.Mathematics.CrossProduct +public import Mathlib.LinearAlgebra.CrossProduct /-! ## Pauli matrices diff --git a/Physlib/Relativity/PauliMatrices/SelfAdjoint.lean b/Physlib/Relativity/PauliMatrices/SelfAdjoint.lean index 9a3ceab64b..91d2279493 100644 --- a/Physlib/Relativity/PauliMatrices/SelfAdjoint.lean +++ b/Physlib/Relativity/PauliMatrices/SelfAdjoint.lean @@ -7,7 +7,9 @@ module public import Physlib.Relativity.PauliMatrices.Basic public import Physlib.Relativity.MinkowskiMatrix -public import Mathlib.Analysis.CStarAlgebra.Matrix +public import Mathlib.Analysis.CStarAlgebra.Classes +public import Mathlib.Analysis.InnerProductSpace.Basic +public import Mathlib.Tactic.Positivity /-! ## Interaction of Pauli matrices with self-adjoint matrices diff --git a/Physlib/Relativity/SL2C/AxisRotations.lean b/Physlib/Relativity/SL2C/AxisRotations.lean index a4b8022ff6..7ed75206d8 100644 --- a/Physlib/Relativity/SL2C/AxisRotations.lean +++ b/Physlib/Relativity/SL2C/AxisRotations.lean @@ -5,7 +5,9 @@ Authors: Jinzheng Li, Nathaneal Sajan, Joseph Tooby-Smith -/ module -public import Physlib.Relativity.SL2C.Basic +public import Mathlib.Analysis.Real.Sqrt +public import Mathlib.Basic.Complex.Basic +public import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup /-! # Coordinate-axis rotations in `SL(2,ℂ)` diff --git a/Physlib/Relativity/SL2C/Basic.lean b/Physlib/Relativity/SL2C/Basic.lean index e61a1684f2..106d604f39 100644 --- a/Physlib/Relativity/SL2C/Basic.lean +++ b/Physlib/Relativity/SL2C/Basic.lean @@ -8,6 +8,7 @@ module public import Physlib.Relativity.SL2C.SelfAdjoint public import Mathlib.Analysis.Complex.Polynomial.Basic public import Physlib.Relativity.LorentzGroup.Restricted.Basic +public import Physlib.Mathematics.SchurTriangulation /-! # The group SL(2, ℂ) and it's relation to the Lorentz group diff --git a/Physlib/Relativity/SL2C/SelfAdjoint.lean b/Physlib/Relativity/SL2C/SelfAdjoint.lean index d8e873171c..85d5de8eb8 100644 --- a/Physlib/Relativity/SL2C/SelfAdjoint.lean +++ b/Physlib/Relativity/SL2C/SelfAdjoint.lean @@ -5,8 +5,11 @@ Authors: Gordon Hsu -/ module -public import Physlib.Mathematics.SchurTriangulation public import Mathlib.LinearAlgebra.Matrix.Hermitian +public import Mathlib.Analysis.InnerProductSpace.Basic +public import Mathlib.LinearAlgebra.Determinant +public import Mathlib.LinearAlgebra.Matrix.Block +public import Mathlib.LinearAlgebra.Matrix.SchurComplement /-! # Extra lemmas regarding `Lorentz.SL2C.toSelfAdjointMap` This file redefines `Lorentz.SL2C.toSelfAdjointMap` by dropping the special linear condition for its diff --git a/Physlib/Relativity/Tensors/Basic.lean b/Physlib/Relativity/Tensors/Basic.lean index d09b71ed9c..eab9e25337 100644 --- a/Physlib/Relativity/Tensors/Basic.lean +++ b/Physlib/Relativity/Tensors/Basic.lean @@ -5,12 +5,11 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Relativity.Tensors.ComponentIdx.Single public import Physlib.Relativity.Tensors.Reindexing -public import Physlib.Relativity.Tensors.Contraction.SuccSuccAbove public import Mathlib.Topology.Algebra.Module.ModuleTopology public import Mathlib.Analysis.RCLike.Basic public import Mathlib.Tactic.Cases +public import Physlib.Relativity.Tensors.ComponentIdx.Basic /-! # Tensors diff --git a/Physlib/Relativity/Tensors/Conjugation/Basic.lean b/Physlib/Relativity/Tensors/Conjugation/Basic.lean index 3d96af0cdf..f63d7cbdd9 100644 --- a/Physlib/Relativity/Tensors/Conjugation/Basic.lean +++ b/Physlib/Relativity/Tensors/Conjugation/Basic.lean @@ -5,11 +5,8 @@ Authors: Andrea Pari -/ module -public import Physlib.Relativity.Tensors.Contraction.Basic public import Physlib.Relativity.Tensors.Contraction.Basis public import Physlib.Mathematics.ConjModule -public import Mathlib.Algebra.Star.Basic -public import Mathlib.LinearAlgebra.Finsupp.LSum /-! diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index cd86320bfe..7b4e84389c 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith module public import Mathlib.Data.Finset.Sort -public import Mathlib.Data.Nat.SuccPred /-! # Defining succSuccAbove diff --git a/Physlib/Relativity/Tensors/Evaluation.lean b/Physlib/Relativity/Tensors/Evaluation.lean index 2a7cab9388..7675451a2e 100644 --- a/Physlib/Relativity/Tensors/Evaluation.lean +++ b/Physlib/Relativity/Tensors/Evaluation.lean @@ -7,7 +7,7 @@ module public import Physlib.Relativity.Tensors.Product public import Physlib.Relativity.Tensors.Contraction.Basis -public import Physlib.Meta.Sorry +public import Physlib.Relativity.Tensors.ComponentIdx.Single /-! # Evaluation of tensor indices diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean index 34e0ea8eb8..56e9df2baf 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Basic.lean @@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.Tensors.RealTensor.Metrics.Pre -public import Physlib.Relativity.Tensors.Contraction.Basis public import Physlib.Relativity.Tensors.Elab /-! diff --git a/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean index f3ac357874..05aadb0469 100644 --- a/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean +++ b/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean @@ -6,7 +6,7 @@ Authors: Matteo Cipollina, Joseph Tooby-Smith module public import Mathlib.Analysis.InnerProductSpace.PiL2 -public import Mathlib.Geometry.Manifold.IsManifold.Basic +public import Mathlib.Geometry.Manifold.ChartedSpace /-! # Lorentz co vectors diff --git a/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean b/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean index 6f3de12bc0..56af8b1bd5 100644 --- a/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean +++ b/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean @@ -7,7 +7,6 @@ module public import Physlib.Relativity.Tensors.RealTensor.CoVector.Basic public import Physlib.Relativity.Tensors.RealTensor.Basic -public import Mathlib.Geometry.Manifold.ChartedSpace /-! # Tensorial nature of Lorentz covectors diff --git a/Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean b/Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean index 86083f53de..c3a1817404 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean @@ -16,7 +16,7 @@ public import Mathlib.LinearAlgebra.TensorProduct.Matrix @[expose] public section noncomputable section -open Matrix Module MatrixGroups Complex TensorProduct CategoryTheory.MonoidalCategory +open Matrix Module MatrixGroups Complex TensorProduct namespace Lorentz diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean index c07df048cb..53e83a5a09 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Modules -public import Mathlib.RepresentationTheory.Rep.Basic +public import Mathlib.RepresentationTheory.Intertwining /-! # Real Lorentz vectors @@ -107,8 +107,6 @@ lemma coBasisFin_toFin1dℝ {d : ℕ} (i : Fin (1 + d)) : lemma coBasisFin_repr_apply {d : ℕ} (p : CoMod d) (i : Fin (1 + d)) : (coBasisFin d).repr p i = p.val (finSumFinEquiv.symm i) := by rfl -open CategoryTheory.MonoidalCategory - /-! ## Isomorphism between contravariant and covariant Lorentz vectors diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean index 06fc785a6e..3b621ebb12 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean @@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Basic +public import Mathlib.RepresentationTheory.Rep.Basic /-! # Contraction of Real Lorentz vectors diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean index a484048a72..d788830e7a 100644 --- a/Physlib/Relativity/Tensors/Reindexing.lean +++ b/Physlib/Relativity/Tensors/Reindexing.lean @@ -5,11 +5,7 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Relativity.Tensors.ComponentIdx.Single public import Physlib.Relativity.Tensors.Contraction.SuccSuccAbove -public import Mathlib.Topology.Algebra.Module.ModuleTopology -public import Mathlib.Analysis.RCLike.Basic -public import Mathlib.Tactic.Cases public import Mathlib.GroupTheory.Perm.Fin /-! @@ -68,11 +64,7 @@ end Fin namespace TensorSpecies -variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G] - {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)] - {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)] - {rep : (c : C) → Representation k G (V c)} {b : (c : C) → Basis (basisIdx c) k (V c)} - (S : TensorSpecies k C G V basisIdx rep b) +variable {C : Type} namespace Tensor diff --git a/Physlib/Relativity/Tensors/TensorSpecies/Basic.lean b/Physlib/Relativity/Tensors/TensorSpecies/Basic.lean index 1146702163..684a4bb09d 100644 --- a/Physlib/Relativity/Tensors/TensorSpecies/Basic.lean +++ b/Physlib/Relativity/Tensors/TensorSpecies/Basic.lean @@ -5,10 +5,9 @@ Authors: Joseph Tooby-Smith -/ module -public import Mathlib.RepresentationTheory.Rep.Basic -public import Physlib.Mathematics.PiTensorProduct -public import Mathlib.Algebra.Lie.OfAssociative public import Physlib.Meta.TODO.Basic +public import Mathlib.LinearAlgebra.PiTensorProduct.Basic +public import Mathlib.RepresentationTheory.Intertwining /-! # Tensor species diff --git a/Physlib/Relativity/Tensors/Tensorial.lean b/Physlib/Relativity/Tensors/Tensorial.lean index 97e4064467..f665f03e2e 100644 --- a/Physlib/Relativity/Tensors/Tensorial.lean +++ b/Physlib/Relativity/Tensors/Tensorial.lean @@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Relativity.Tensors.Product public import Physlib.Relativity.Tensors.Evaluation public import Mathlib.Topology.Algebra.Module.FiniteDimension /-! diff --git a/Physlib/SpaceAndTime/ReferenceFrame.lean b/Physlib/SpaceAndTime/ReferenceFrame.lean index 869c31cf00..9ada42f576 100644 --- a/Physlib/SpaceAndTime/ReferenceFrame.lean +++ b/Physlib/SpaceAndTime/ReferenceFrame.lean @@ -5,10 +5,9 @@ Authors: Raunak Chhatwal -/ module -public import Mathlib.LinearAlgebra.AffineSpace.Basis -public import Mathlib.Topology.Algebra.Module.TransferInstance public import Physlib.SpaceAndTime.Space.Basic public import Physlib.SpaceAndTime.Time.Basic +public import Mathlib.Topology.Homeomorph.TransferInstance /-! # Reference frames diff --git a/Physlib/SpaceAndTime/Space/Basic.lean b/Physlib/SpaceAndTime/Space/Basic.lean index 794987c575..2349171542 100644 --- a/Physlib/SpaceAndTime/Space/Basic.lean +++ b/Physlib/SpaceAndTime/Space/Basic.lean @@ -5,8 +5,6 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Meta.TODO.Basic -public import Mathlib.Analysis.InnerProductSpace.PiL2 public import Mathlib.Geometry.Manifold.Instances.Real /-! diff --git a/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean b/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean index 7449bfe81c..a1bd0c3752 100644 --- a/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean +++ b/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean @@ -8,7 +8,6 @@ module public import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension public import Physlib.SpaceAndTime.Space.Derivatives.Basic public import Physlib.SpaceAndTime.Space.Slice -public import Mathlib.Analysis.Calculus.ParametricIntegral /-! # Constant slice distributions diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Basic.lean b/Physlib/SpaceAndTime/Space/Derivatives/Basic.lean index 668d1f90d3..d2f4db9d06 100644 --- a/Physlib/SpaceAndTime/Space/Derivatives/Basic.lean +++ b/Physlib/SpaceAndTime/Space/Derivatives/Basic.lean @@ -9,7 +9,6 @@ public import Mathlib.Analysis.Calculus.FDeriv.Symmetric public import Physlib.Mathematics.Distribution.Basic public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic public import Physlib.SpaceAndTime.Space.Module -public import Mathlib.Analysis.InnerProductSpace.Calculus public import Mathlib.Geometry.Manifold.MFDeriv.NormedSpace /-! diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean b/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean index 427896d815..9cb808787c 100644 --- a/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean +++ b/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean @@ -8,8 +8,8 @@ module public import Physlib.SpaceAndTime.Space.Derivatives.Laplacian public import Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare public import Physlib.SpaceAndTime.Space.CrossProduct -public import Mathlib.Analysis.Calculus.ParametricIntervalIntegral public import Physlib.Mathematics.LeviCivita.Basic +public import Mathlib.Tactic.Cases /-! diff --git a/Physlib/SpaceAndTime/Space/DistOfFunction.lean b/Physlib/SpaceAndTime/Space/DistOfFunction.lean index 0fd7769286..a60d87ba8b 100644 --- a/Physlib/SpaceAndTime/Space/DistOfFunction.lean +++ b/Physlib/SpaceAndTime/Space/DistOfFunction.lean @@ -8,7 +8,6 @@ module public import Physlib.SpaceAndTime.Space.IsDistBounded public import Physlib.SpaceAndTime.Space.Derivatives.Basic public import Mathlib.MeasureTheory.SpecificCodomains.WithLp -public import Physlib.Mathematics.Distribution.Basic /-! # Distributions from functions on space diff --git a/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean b/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean index a9086fbbed..44f0e66d71 100644 --- a/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean +++ b/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean @@ -6,9 +6,6 @@ Authors: Gregory J. Loges module public import Physlib.SpaceAndTime.Space.IsDistBounded -public import Physlib.SpaceAndTime.Space.Module -public import Mathlib.MeasureTheory.Constructions.HaarToSphere -public import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals /-! # Integrability of norm powers on subsets of Space diff --git a/Physlib/SpaceAndTime/Space/LengthUnit.lean b/Physlib/SpaceAndTime/Space/LengthUnit.lean index d4f9e7a313..4eb56ef37e 100644 --- a/Physlib/SpaceAndTime/Space/LengthUnit.lean +++ b/Physlib/SpaceAndTime/Space/LengthUnit.lean @@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith module public import Physlib.Units.PositiveRealUnit -public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic /-! # Units on Length diff --git a/Physlib/SpaceAndTime/Space/Module.lean b/Physlib/SpaceAndTime/Space/Module.lean index 9d08b88b54..7779e15d98 100644 --- a/Physlib/SpaceAndTime/Space/Module.lean +++ b/Physlib/SpaceAndTime/Space/Module.lean @@ -8,7 +8,6 @@ module public import Physlib.SpaceAndTime.Space.Origin public import Mathlib.Analysis.Distribution.TemperateGrowth public import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace -public import Mathlib.Tactic.Cases /-! # The structure of a module on Space diff --git a/Physlib/SpaceAndTime/Space/Norm/Regularized.lean b/Physlib/SpaceAndTime/Space/Norm/Regularized.lean index e943ae7738..b74ad2fabc 100644 --- a/Physlib/SpaceAndTime/Space/Norm/Regularized.lean +++ b/Physlib/SpaceAndTime/Space/Norm/Regularized.lean @@ -5,8 +5,7 @@ Authors: Gregory J. Loges -/ module -public import Physlib.SpaceAndTime.Space.Derivatives.Basic -public import Physlib.SpaceAndTime.Space.Integrals.NormPow +public import Physlib.SpaceAndTime.Space.Module /-! # Regularized powers of the norm on space diff --git a/Physlib/SpaceAndTime/Space/SmoothFunctions.lean b/Physlib/SpaceAndTime/Space/SmoothFunctions.lean index 4d1145fba3..855364a4ca 100644 --- a/Physlib/SpaceAndTime/Space/SmoothFunctions.lean +++ b/Physlib/SpaceAndTime/Space/SmoothFunctions.lean @@ -6,7 +6,6 @@ Authors: Giuseppe Sorge module public import Physlib.SpaceAndTime.Space.Module -public import Mathlib.Geometry.Manifold.ContMDiffMap /-! # Smooth real-valued functions on space diff --git a/Physlib/SpaceAndTime/SpaceTime/Basic.lean b/Physlib/SpaceAndTime/SpaceTime/Basic.lean index 7e75be7608..0b6d38a7cd 100644 --- a/Physlib/SpaceAndTime/SpaceTime/Basic.lean +++ b/Physlib/SpaceAndTime/SpaceTime/Basic.lean @@ -10,7 +10,6 @@ public import Physlib.Relativity.SpeedOfLight public import Physlib.SpaceAndTime.Space.EuclideanGroup.Action public import Physlib.SpaceAndTime.Space.Integrals.Basic public import Physlib.SpaceAndTime.Time.InnerProductSpace -public import Physlib.Meta.Informal.Basic /-! # Spacetime diff --git a/Physlib/SpaceAndTime/Time/Basic.lean b/Physlib/SpaceAndTime/Time/Basic.lean index 2910958371..5839c61513 100644 --- a/Physlib/SpaceAndTime/Time/Basic.lean +++ b/Physlib/SpaceAndTime/Time/Basic.lean @@ -5,10 +5,7 @@ Authors: Joseph Tooby-Smith -/ module -public import Mathlib.Analysis.Normed.Group.AddTorsor -public import Mathlib.Analysis.Normed.Group.Real public import Mathlib.Geometry.Manifold.IsManifold.Basic -public import Mathlib.LinearAlgebra.AffineSpace.Defs /-! # Time diff --git a/Physlib/SpaceAndTime/Time/InnerProductSpace.lean b/Physlib/SpaceAndTime/Time/InnerProductSpace.lean index ddbcb62a2c..45717ea6f6 100644 --- a/Physlib/SpaceAndTime/Time/InnerProductSpace.lean +++ b/Physlib/SpaceAndTime/Time/InnerProductSpace.lean @@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith -/ module -public import Mathlib.Analysis.Calculus.FDeriv.Linear public import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace public import Physlib.SpaceAndTime.Time.Basic /-! diff --git a/Physlib/SpaceAndTime/Time/TimeUnit.lean b/Physlib/SpaceAndTime/Time/TimeUnit.lean index be648cd80e..5ee4dd0f81 100644 --- a/Physlib/SpaceAndTime/Time/TimeUnit.lean +++ b/Physlib/SpaceAndTime/Time/TimeUnit.lean @@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith module public import Physlib.Units.PositiveRealUnit -public import Mathlib.Analysis.RCLike.Basic /-! # Units on time diff --git a/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/Basic.lean b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/Basic.lean index afc1098602..17c69007c4 100644 --- a/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/Basic.lean +++ b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/Basic.lean @@ -5,9 +5,7 @@ Authors: Alex Meiburg -/ module -public import Mathlib.MeasureTheory.Constructions.Pi public import Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop -public import Physlib.Meta.Sorry /-! ## The Microcanonical Ensemble diff --git a/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean b/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean index ad432dcd58..7f952c25cb 100644 --- a/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean +++ b/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean @@ -5,7 +5,9 @@ Authors: Joseph Tooby-Smith -/ module -public import Mathlib.Analysis.Normed.Ring.Lemmas +public import Mathlib.Algebra.BigOperators.Group.Multiset.Basic +public import Mathlib.Tactic.Ring.RingNF + /-! # Fluxes of representations diff --git a/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/ChiralIndices.lean b/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/ChiralIndices.lean index eed9fe57d9..8860d1392a 100644 --- a/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/ChiralIndices.lean +++ b/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/ChiralIndices.lean @@ -6,6 +6,11 @@ Authors: Joseph Tooby-Smith module public import Physlib.StringTheory.FTheory.SU5.Fluxes.Basic +public import Mathlib.Algebra.Order.BigOperators.Group.Multiset +public import Mathlib.Algebra.Order.Group.Int +public import Mathlib.Algebra.Order.Sub.Basic +public import Mathlib.Data.Finset.Insert +public import Mathlib.Data.Multiset.OrderedMonoid /-! # Constraints on chiral indices from the condition of no chiral exotics diff --git a/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Elems.lean b/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Elems.lean index 4ddfb0738d..280a95c112 100644 --- a/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Elems.lean +++ b/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Elems.lean @@ -6,6 +6,9 @@ Authors: Joseph Tooby-Smith module public import Physlib.StringTheory.FTheory.SU5.Fluxes.Basic +public import Mathlib.Data.Finset.Card +public import Mathlib.Data.Multiset.Powerset +public import Mathlib.Tactic.FinCases /-! # Terms of `FluxesFive` and `FluxesTen` with no chiral exotics diff --git a/Physlib/StringTheory/FTheory/SU5/Quanta/FiveQuanta.lean b/Physlib/StringTheory/FTheory/SU5/Quanta/FiveQuanta.lean index 17619bdc3e..a2cd1b8d1a 100644 --- a/Physlib/StringTheory/FTheory/SU5/Quanta/FiveQuanta.lean +++ b/Physlib/StringTheory/FTheory/SU5/Quanta/FiveQuanta.lean @@ -7,6 +7,8 @@ module public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.OfFinset public import Physlib.StringTheory.FTheory.SU5.Fluxes.NoExotics.Completeness +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Algebra.Group.Action.Defs /-! # Quanta of 5-d representations diff --git a/Physlib/StringTheory/FTheory/SU5/Quanta/IsViable.lean b/Physlib/StringTheory/FTheory/SU5/Quanta/IsViable.lean index af86831902..b1a29a134f 100644 --- a/Physlib/StringTheory/FTheory/SU5/Quanta/IsViable.lean +++ b/Physlib/StringTheory/FTheory/SU5/Quanta/IsViable.lean @@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.StringTheory.FTheory.SU5.Charges.AnomalyFree +public import Mathlib.Data.ZMod.Defs /-! # Viable Quanta with Yukawa diff --git a/Physlib/StringTheory/FTheory/SU5/Quanta/TenQuanta.lean b/Physlib/StringTheory/FTheory/SU5/Quanta/TenQuanta.lean index ec06dd74b4..007c21f007 100644 --- a/Physlib/StringTheory/FTheory/SU5/Quanta/TenQuanta.lean +++ b/Physlib/StringTheory/FTheory/SU5/Quanta/TenQuanta.lean @@ -7,6 +7,8 @@ module public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.OfFinset public import Physlib.StringTheory.FTheory.SU5.Fluxes.NoExotics.Completeness +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Algebra.Group.Action.Defs /-! # Quanta of 10d representations diff --git a/Physlib/Thermodynamics/Temperature/TemperatureUnits.lean b/Physlib/Thermodynamics/Temperature/TemperatureUnits.lean index 514ba2d943..1f494e182b 100644 --- a/Physlib/Thermodynamics/Temperature/TemperatureUnits.lean +++ b/Physlib/Thermodynamics/Temperature/TemperatureUnits.lean @@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith module public import Physlib.Units.PositiveRealUnit -public import Mathlib.Analysis.RCLike.Basic /-! # Units on Temperature diff --git a/Physlib/Units/Dimension.lean b/Physlib/Units/Dimension.lean index 63e8f10643..a3e8a5f329 100644 --- a/Physlib/Units/Dimension.lean +++ b/Physlib/Units/Dimension.lean @@ -5,9 +5,8 @@ Authors: Joseph Tooby-Smith -/ module -public import Mathlib.Analysis.Normed.Field.Lemmas -public import Mathlib.Tactic.DeriveFintype public import Physlib.Units.Exponent +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic /-! # Dimension @@ -35,8 +34,6 @@ a suitable basis `B`. @[expose] public section -open NNReal - /-! ## Defining dimensions diff --git a/Physlib/Units/ISQBridge.lean b/Physlib/Units/ISQBridge.lean index c005cd31ff..a4ecf3dd2e 100644 --- a/Physlib/Units/ISQBridge.lean +++ b/Physlib/Units/ISQBridge.lean @@ -7,6 +7,8 @@ module public import Physlib.Units.LTMCTDimensionBase public import Physlib.Units.ISQDimensionBase +public import Mathlib.Tactic.Ring +public import Mathlib.Tactic.Linarith /-! # Bridging PhysLib's default basis and the ISQ basis diff --git a/Physlib/Units/ISQDimensionBase.lean b/Physlib/Units/ISQDimensionBase.lean index bc717ac951..3deb25fa68 100644 --- a/Physlib/Units/ISQDimensionBase.lean +++ b/Physlib/Units/ISQDimensionBase.lean @@ -6,6 +6,7 @@ Authors: Nicolas Rouquette module public import Physlib.Units.Dimension +public import Mathlib.Data.Fintype.Card /-! # The ISQ base quantities diff --git a/Physlib/Units/SIUnitChoices.lean b/Physlib/Units/SIUnitChoices.lean index 71db7653d0..8c8a023c23 100644 --- a/Physlib/Units/SIUnitChoices.lean +++ b/Physlib/Units/SIUnitChoices.lean @@ -6,7 +6,6 @@ Authors: Nicolas Rouquette module public import Physlib.Units.UnitSystem -public import Physlib.Units.PositiveRealUnit public import Physlib.Units.ISQDimensionBase /-! diff --git a/Physlib/Units/WithDim/Analysis.lean b/Physlib/Units/WithDim/Analysis.lean index 31022c235b..3d0d8dc2b2 100644 --- a/Physlib/Units/WithDim/Analysis.lean +++ b/Physlib/Units/WithDim/Analysis.lean @@ -7,7 +7,6 @@ module public import Physlib.Units.WithDim.Basic public import Mathlib.Analysis.Calculus.FDeriv.Equiv -public import Mathlib.Analysis.Normed.Group.Basic /-! # A. Analysis of dimension-tagged quantities diff --git a/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/State/DensityUncertainty.lean b/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/State/DensityUncertainty.lean index 5d46c434fe..c08f210d65 100644 --- a/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/State/DensityUncertainty.lean +++ b/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/State/DensityUncertainty.lean @@ -8,6 +8,7 @@ module public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.Uncertainty public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.State.Density public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.State.Vector +public import Mathlib.Analysis.InnerProductSpace.Trace /-! diff --git a/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/State/Vector.lean b/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/State/Vector.lean index 3c8b46d564..a1e17d459f 100644 --- a/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/State/Vector.lean +++ b/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/State/Vector.lean @@ -7,7 +7,7 @@ module public import PhyslibAlpha.ProbabilisticTheory.StarAlgebra.Restrict public import PhyslibAlpha.ProbabilisticTheory.State.Basic -public import Mathlib +public import Mathlib.Analysis.InnerProductSpace.StarOrder /-! diff --git a/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/Trace.lean b/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/Trace.lean index 9bb4abaa1f..c898e04496 100644 --- a/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/Trace.lean +++ b/PhyslibAlpha/ProbabilisticTheory/HilbertSpace/Trace.lean @@ -5,7 +5,8 @@ Authors: David Gross -/ module -public import Mathlib +public import Mathlib.Analysis.InnerProductSpace.StarOrder +public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic public import PhyslibAlpha.ProbabilisticTheory.StarAlgebra.Traciality /-! diff --git a/PhyslibAlpha/QuantumMechanics/StinespringDilation.lean b/PhyslibAlpha/QuantumMechanics/StinespringDilation.lean index e9449628cb..a4a73f891a 100644 --- a/PhyslibAlpha/QuantumMechanics/StinespringDilation.lean +++ b/PhyslibAlpha/QuantumMechanics/StinespringDilation.lean @@ -8,7 +8,7 @@ public import Mathlib.Data.Matrix.PEquiv public import Mathlib.Probability.Distributions.Poisson.Basic public import Mathlib.Analysis.Normed.Lp.lpSpace public import Physlib.Meta.TODO.Basic -public import Mathlib +public import Mathlib.Analysis.Matrix.Order /-! # Stinespring dilation -/ diff --git a/QuantumInfo/Capacity/Capacity.lean b/QuantumInfo/Capacity/Capacity.lean index 1a3298941d..da2bfd6a94 100644 --- a/QuantumInfo/Capacity/Capacity.lean +++ b/QuantumInfo/Capacity/Capacity.lean @@ -8,17 +8,11 @@ module public import Mathlib.Analysis.SpecialFunctions.Log.Base public import QuantumInfo.Entropy.VonNeumann -public import QuantumInfo.Entropy.SSA -public import QuantumInfo.Entropy.Relative -public import QuantumInfo.Entropy.DPI public import QuantumInfo.Channels.Bundled public import QuantumInfo.Channels.CPTP -public import QuantumInfo.Channels.Dual public import QuantumInfo.Channels.MatrixMap public import QuantumInfo.Channels.Unbundled public import QuantumInfo.States.Mixed.Fidelity -public import QuantumInfo.States.Mixed.TraceDistance -public import Physlib.Meta.Sorry /-! # Quantum Capacity diff --git a/QuantumInfo/Channels/DegradableOrder.lean b/QuantumInfo/Channels/DegradableOrder.lean index d6d213f0da..efd821016b 100644 --- a/QuantumInfo/Channels/DegradableOrder.lean +++ b/QuantumInfo/Channels/DegradableOrder.lean @@ -7,7 +7,6 @@ module public import QuantumInfo.Channels.Bundled public import QuantumInfo.Channels.CPTP -public import QuantumInfo.Channels.Dual public import QuantumInfo.Channels.MatrixMap public import QuantumInfo.Channels.Unbundled diff --git a/QuantumInfo/Channels/Dual.lean b/QuantumInfo/Channels/Dual.lean index 08b2e7494c..e254bf5d3a 100644 --- a/QuantumInfo/Channels/Dual.lean +++ b/QuantumInfo/Channels/Dual.lean @@ -6,7 +6,6 @@ Authors: Alex Meiburg, Dennj Osele module public import QuantumInfo.Channels.Bundled -public import Mathlib.LinearAlgebra.Matrix.FiniteDimensional /-! # Duals of matrix map diff --git a/QuantumInfo/Channels/MatrixMap.lean b/QuantumInfo/Channels/MatrixMap.lean index 1c58f9e2fc..6334aa0087 100644 --- a/QuantumInfo/Channels/MatrixMap.lean +++ b/QuantumInfo/Channels/MatrixMap.lean @@ -5,23 +5,17 @@ Authors: Alex Meiburg -/ module -public import Mathlib.LinearAlgebra.TensorProduct.Matrix public import Mathlib.LinearAlgebra.PiTensorProduct.Basic public import Mathlib.LinearAlgebra.PiTensorProduct.Basis public import Mathlib.Data.Set.Card public import Mathlib.Algebra.Module.LinearMap.Basic public import QuantumInfo.ForMathlib.ContinuousLinearMap -public import QuantumInfo.ForMathlib.ComplexLaplaceTransform -public import QuantumInfo.ForMathlib.ContinuousSup -public import QuantumInfo.ForMathlib.Filter public import QuantumInfo.ForMathlib.HermitianMat public import QuantumInfo.ForMathlib.Isometry public import QuantumInfo.ForMathlib.LinearEquiv public import QuantumInfo.ForMathlib.MatrixNorm.TraceNorm public import QuantumInfo.ForMathlib.Matrix -public import QuantumInfo.ForMathlib.Minimax public import QuantumInfo.ForMathlib.Misc -public import QuantumInfo.ForMathlib.Unitary public import QuantumInfo.States.Pure.Braket public import QuantumInfo.States.Mixed.MState diff --git a/QuantumInfo/Channels/Pinching.lean b/QuantumInfo/Channels/Pinching.lean index b6657656f1..b4534cffcd 100644 --- a/QuantumInfo/Channels/Pinching.lean +++ b/QuantumInfo/Channels/Pinching.lean @@ -7,14 +7,11 @@ module public import QuantumInfo.Channels.Bundled public import QuantumInfo.Channels.CPTP -public import QuantumInfo.Channels.Dual public import QuantumInfo.Channels.MatrixMap public import QuantumInfo.Channels.Unbundled public import QuantumInfo.States.Mixed.MState public import QuantumInfo.Entropy.VonNeumann -public import QuantumInfo.Entropy.SSA public import QuantumInfo.Entropy.Relative -public import QuantumInfo.Entropy.DPI public import QuantumInfo.ForMathlib.HermitianMat.CFC /-! # Pinching channels diff --git a/QuantumInfo/Channels/Unbundled.lean b/QuantumInfo/Channels/Unbundled.lean index 3719fecaab..8a0318739e 100644 --- a/QuantumInfo/Channels/Unbundled.lean +++ b/QuantumInfo/Channels/Unbundled.lean @@ -7,6 +7,7 @@ module public import QuantumInfo.Channels.MatrixMap public import QuantumInfo.ForMathlib.MatrixNorm.TraceNorm +public import Mathlib.LinearAlgebra.Matrix.Bilinear /-! # Properties of Matrix Maps diff --git a/QuantumInfo/ClassicalInfo/Channel.lean b/QuantumInfo/ClassicalInfo/Channel.lean index 1bfbcbab16..f3ee902845 100644 --- a/QuantumInfo/ClassicalInfo/Channel.lean +++ b/QuantumInfo/ClassicalInfo/Channel.lean @@ -6,7 +6,6 @@ Authors: Alex Meiburg module public import QuantumInfo.ClassicalInfo.Distribution -public import Mathlib.MeasureTheory.Measure.MeasureSpaceDef @[expose] public section diff --git a/QuantumInfo/ClassicalInfo/Prob.lean b/QuantumInfo/ClassicalInfo/Prob.lean index 796c3d1b4e..381658e4a0 100644 --- a/QuantumInfo/ClassicalInfo/Prob.lean +++ b/QuantumInfo/ClassicalInfo/Prob.lean @@ -5,13 +5,13 @@ Authors: Alex Meiburg -/ module -public import Mathlib.Analysis.Convex.Mul public import Mathlib.Analysis.SpecialFunctions.Log.Basic public import Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog public import Mathlib.Basic.NNReal.Basic public import Mathlib.Data.EReal.Basic public import Mathlib.Tactic.Finiteness public import Mathlib.Topology.UnitInterval +public import Mathlib.Analysis.Convex.Basic /-! # Probabilities diff --git a/QuantumInfo/Entropy/DPI.lean b/QuantumInfo/Entropy/DPI.lean index aa4cee1f59..54c7d00512 100644 --- a/QuantumInfo/Entropy/DPI.lean +++ b/QuantumInfo/Entropy/DPI.lean @@ -8,6 +8,7 @@ module public import QuantumInfo.Entropy.Relative public import QuantumInfo.ForMathlib.HermitianMat.Sqrt public import QuantumInfo.ForMathlib.HermitianMat.LiebConcavity +public import Mathlib.Data.Fintype.Shrink @[expose] public section diff --git a/QuantumInfo/Entropy/Relative.lean b/QuantumInfo/Entropy/Relative.lean index cd6b81a2af..554cf9b13b 100644 --- a/QuantumInfo/Entropy/Relative.lean +++ b/QuantumInfo/Entropy/Relative.lean @@ -6,7 +6,7 @@ Authors: Alex Meiburg module public import QuantumInfo.Entropy.VonNeumann -public import Physlib.Meta.Sorry +public import QuantumInfo.ForMathlib.Minimax @[expose] public section diff --git a/QuantumInfo/Entropy/VonNeumann.lean b/QuantumInfo/Entropy/VonNeumann.lean index aeee3d3e25..a3798da2f6 100644 --- a/QuantumInfo/Entropy/VonNeumann.lean +++ b/QuantumInfo/Entropy/VonNeumann.lean @@ -8,10 +8,10 @@ module public import QuantumInfo.States.Pure.Braket public import QuantumInfo.Channels.Bundled public import QuantumInfo.Channels.CPTP -public import QuantumInfo.Channels.Dual public import QuantumInfo.Channels.MatrixMap public import QuantumInfo.Channels.Unbundled public import QuantumInfo.ClassicalInfo.Entropy +public import Mathlib.Data.Multiset.Functor /-! Quantum notions of information and entropy. diff --git a/QuantumInfo/ForMathlib/ContinuousSup.lean b/QuantumInfo/ForMathlib/ContinuousSup.lean index a8ea0c1d0e..2240be7f53 100644 --- a/QuantumInfo/ForMathlib/ContinuousSup.lean +++ b/QuantumInfo/ForMathlib/ContinuousSup.lean @@ -5,10 +5,9 @@ Authors: Alex Meiburg -/ module -public import Mathlib.Analysis.InnerProductSpace.Basic public import Mathlib.Analysis.Normed.Module.FiniteDimension -public import Mathlib.Algebra.Order.Star.Real public import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps +public import Mathlib.Analysis.InnerProductSpace.Defs @[expose] public section diff --git a/QuantumInfo/ForMathlib/Filter.lean b/QuantumInfo/ForMathlib/Filter.lean index 4dcb0ac461..9d2537f789 100644 --- a/QuantumInfo/ForMathlib/Filter.lean +++ b/QuantumInfo/ForMathlib/Filter.lean @@ -5,7 +5,9 @@ Authors: Alex Meiburg -/ module -public import Mathlib +public import Mathlib.Algebra.Order.Floor.Semifield +public import Mathlib.Analysis.RCLike.Basic +public import Mathlib.Analysis.SpecificLimits.Basic public import Mathlib.Tactic.Bound diff --git a/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/JensenOperatorInequalityIVtoV.lean b/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/JensenOperatorInequalityIVtoV.lean index 13c2628a0a..50e1eaea2b 100644 --- a/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/JensenOperatorInequalityIVtoV.lean +++ b/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/JensenOperatorInequalityIVtoV.lean @@ -7,7 +7,6 @@ module public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.BlockDiagonal public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.LownerHeinzTheorem -public import Mathlib.Analysis.CStarAlgebra.Unitary.Span @[expose] public section diff --git a/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/LiebAndoTrace.lean b/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/LiebAndoTrace.lean index 5d134f526f..7e7fc0ccab 100644 --- a/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/LiebAndoTrace.lean +++ b/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/LiebAndoTrace.lean @@ -7,9 +7,7 @@ module public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.OperatorGeometricMean public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.HilbertSchmidtOperatorSpace -public import Mathlib.Analysis.CStarAlgebra.Matrix public import Mathlib.Analysis.InnerProductSpace.JointEigenspace -public import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus public import Mathlib.LinearAlgebra.Lagrange public import Mathlib.LinearAlgebra.Trace diff --git a/QuantumInfo/ForMathlib/HermitianMat/Basic.lean b/QuantumInfo/ForMathlib/HermitianMat/Basic.lean index 185a3b15b5..1c8f8c2527 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Basic.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Basic.lean @@ -6,7 +6,6 @@ Authors: Alex Meiburg module public import QuantumInfo.ForMathlib.Matrix -public import QuantumInfo.ForMathlib.IsMaximalSelfAdjoint public import QuantumInfo.ForMathlib.ContinuousLinearMap public import QuantumInfo.ForMathlib.Tactic.Commutes diff --git a/QuantumInfo/ForMathlib/HermitianMat/Inner.lean b/QuantumInfo/ForMathlib/HermitianMat/Inner.lean index 60d60c60a4..a86eed6335 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Inner.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Inner.lean @@ -7,7 +7,6 @@ module public import QuantumInfo.ForMathlib.HermitianMat.Order public import Mathlib.Analysis.Convex.Contractible -public import Mathlib.Topology.Instances.Real.Lemmas /-! # Inner product of Hermitian Matrices diff --git a/QuantumInfo/ForMathlib/HermitianMat/Jordan.lean b/QuantumInfo/ForMathlib/HermitianMat/Jordan.lean index f4848e7906..70496e2b7a 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Jordan.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Jordan.lean @@ -7,7 +7,6 @@ module public import Mathlib.Algebra.Jordan.Basic -public import QuantumInfo.ForMathlib.HermitianMat.CFC public import QuantumInfo.ForMathlib.HermitianMat.Order /-! diff --git a/QuantumInfo/ForMathlib/HermitianMat/NonSingular.lean b/QuantumInfo/ForMathlib/HermitianMat/NonSingular.lean index 94b66f7772..d75bd8b715 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/NonSingular.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/NonSingular.lean @@ -6,7 +6,6 @@ Authors: Alex Meiburg module public import QuantumInfo.ForMathlib.HermitianMat.Order -public import QuantumInfo.ForMathlib.Isometry @[expose] public section diff --git a/QuantumInfo/ForMathlib/HermitianMat/Peierls.lean b/QuantumInfo/ForMathlib/HermitianMat/Peierls.lean index c27cbecfc4..55d414970b 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Peierls.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Peierls.lean @@ -6,7 +6,7 @@ Authors: Alex Meiburg module public import QuantumInfo.ForMathlib.HermitianMat.Sqrt -public import QuantumInfo.ForMathlib.HermitianMat.LiebConcavity +public import QuantumInfo.ForMathlib.HermitianMat.Unitary @[expose] public section diff --git a/QuantumInfo/ForMathlib/HermitianMat/Rpow.lean b/QuantumInfo/ForMathlib/HermitianMat/Rpow.lean index 3d2c413a8d..3dbfc3c972 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Rpow.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Rpow.lean @@ -9,6 +9,7 @@ public import QuantumInfo.ForMathlib.HermitianMat.CompoundMatrix public import QuantumInfo.ForMathlib.HermitianMat.LogExp public import QuantumInfo.ForMathlib.HermitianMat.Sqrt public import QuantumInfo.ForMathlib.HermitianMat.Unitary +public import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals @[expose] public section diff --git a/QuantumInfo/ForMathlib/HermitianMat/Trace.lean b/QuantumInfo/ForMathlib/HermitianMat/Trace.lean index 19e22b46d2..41ba0f9fa2 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Trace.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Trace.lean @@ -6,6 +6,7 @@ Authors: Alex Meiburg module public import QuantumInfo.ForMathlib.HermitianMat.Reindex +public import QuantumInfo.ForMathlib.IsMaximalSelfAdjoint /-! # Trace of Hermitian Matrices diff --git a/QuantumInfo/ForMathlib/HermitianMat/Unitary.lean b/QuantumInfo/ForMathlib/HermitianMat/Unitary.lean index c5ede42237..41b484c890 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Unitary.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Unitary.lean @@ -6,8 +6,6 @@ Authors: Alex Meiburg module public import QuantumInfo.ForMathlib.HermitianMat.Inner -public import QuantumInfo.ForMathlib.HermitianMat.NonSingular -public import QuantumInfo.ForMathlib.Isometry @[expose] public section diff --git a/QuantumInfo/ForMathlib/IsMaximalSelfAdjoint.lean b/QuantumInfo/ForMathlib/IsMaximalSelfAdjoint.lean index 0d0f01cf28..d169b55fbc 100644 --- a/QuantumInfo/ForMathlib/IsMaximalSelfAdjoint.lean +++ b/QuantumInfo/ForMathlib/IsMaximalSelfAdjoint.lean @@ -5,7 +5,7 @@ Authors: Alex Meiburg -/ module -public import Mathlib.Analysis.Matrix.Normed +public import Mathlib.Analysis.RCLike.Basic /-! # Maximal self-adjoint subrings diff --git a/QuantumInfo/ForMathlib/LimSupInf.lean b/QuantumInfo/ForMathlib/LimSupInf.lean index 94f0095780..9bd01e6f90 100644 --- a/QuantumInfo/ForMathlib/LimSupInf.lean +++ b/QuantumInfo/ForMathlib/LimSupInf.lean @@ -6,12 +6,10 @@ Authors: Alex Meiburg module public import Mathlib.Algebra.Order.Ring.Star -public import Mathlib.Analysis.Normed.Ring.Lemmas public import Mathlib.Data.Finset.Attr public import Mathlib.Data.Int.Star public import Mathlib.Algebra.Order.Star.Real public import Mathlib.Tactic.Bound -public import Mathlib.Tactic.Peel public import Mathlib.Tactic.Common public import Mathlib.Tactic.Continuity public import Mathlib.Tactic.Finiteness.Attr diff --git a/QuantumInfo/ForMathlib/Majorization.lean b/QuantumInfo/ForMathlib/Majorization.lean index f0535e5f4f..c8d3919a67 100644 --- a/QuantumInfo/ForMathlib/Majorization.lean +++ b/QuantumInfo/ForMathlib/Majorization.lean @@ -5,8 +5,9 @@ Authors: Alex Meiburg -/ module -public import Mathlib +public import Mathlib.Data.Set.PowersetCard public import QuantumInfo.ForMathlib.Matrix +public import Mathlib.Tactic.Cases /-! # Majorization and weak log-majorization diff --git a/QuantumInfo/ForMathlib/Matrix.lean b/QuantumInfo/ForMathlib/Matrix.lean index 07b3c3b740..857c0661f7 100644 --- a/QuantumInfo/ForMathlib/Matrix.lean +++ b/QuantumInfo/ForMathlib/Matrix.lean @@ -11,7 +11,6 @@ public import Mathlib.Analysis.CStarAlgebra.Matrix public import Mathlib.Analysis.Matrix.Order public import Mathlib.Analysis.SpecialFunctions.Bernstein public import Mathlib.Analysis.SpecialFunctions.Pow.NNReal -public import Mathlib.Data.Multiset.Functor --Can't believe I'm having to import this public import Mathlib.LinearAlgebra.Matrix.Kronecker public import Mathlib.LinearAlgebra.Matrix.PosDef public import Mathlib.LinearAlgebra.Matrix.IsDiag diff --git a/QuantumInfo/ForMathlib/Tactic/Commutes/Attribute.lean b/QuantumInfo/ForMathlib/Tactic/Commutes/Attribute.lean index d673b60a88..29804290fe 100644 --- a/QuantumInfo/ForMathlib/Tactic/Commutes/Attribute.lean +++ b/QuantumInfo/ForMathlib/Tactic/Commutes/Attribute.lean @@ -5,7 +5,6 @@ Authors: Alex Meiburg -/ module -public import Mathlib.Init public import Aesop.Frontend.Command /-! diff --git a/QuantumInfo/ForMathlib/ULift.lean b/QuantumInfo/ForMathlib/ULift.lean index 82195f7de8..4aaf773061 100644 --- a/QuantumInfo/ForMathlib/ULift.lean +++ b/QuantumInfo/ForMathlib/ULift.lean @@ -5,7 +5,8 @@ Authors: Alex Meiburg -/ module -public import Mathlib +public import Mathlib.Algebra.Field.ULift +public import Mathlib.Analysis.RCLike.Basic /-! # Typeclass instances for `ULift` diff --git a/QuantumInfo/ForMathlib/Unitary.lean b/QuantumInfo/ForMathlib/Unitary.lean index 5b09a3d5b2..88f84bf518 100644 --- a/QuantumInfo/ForMathlib/Unitary.lean +++ b/QuantumInfo/ForMathlib/Unitary.lean @@ -6,8 +6,7 @@ Authors: Alex Meiburg module public import Mathlib.LinearAlgebra.Matrix.Kronecker -public import Mathlib.LinearAlgebra.Matrix.PosDef -public import QuantumInfo.ForMathlib.HermitianMat.Unitary +public import Mathlib.Analysis.InnerProductSpace.Spectrum @[expose] public section diff --git a/QuantumInfo/Measurements/POVM.lean b/QuantumInfo/Measurements/POVM.lean index a9f3cc3769..813bb877d7 100644 --- a/QuantumInfo/Measurements/POVM.lean +++ b/QuantumInfo/Measurements/POVM.lean @@ -7,7 +7,6 @@ module public import QuantumInfo.Channels.Bundled public import QuantumInfo.Channels.CPTP -public import QuantumInfo.Channels.Dual public import QuantumInfo.Channels.MatrixMap public import QuantumInfo.Channels.Unbundled diff --git a/QuantumInfo/ResourceTheory/FreeState.lean b/QuantumInfo/ResourceTheory/FreeState.lean index 45c83fee00..5b89379f18 100644 --- a/QuantumInfo/ResourceTheory/FreeState.lean +++ b/QuantumInfo/ResourceTheory/FreeState.lean @@ -8,16 +8,12 @@ module public import Mathlib.Algebra.Module.Submodule.Lattice public import Mathlib.Analysis.Subadditive public import Mathlib.CategoryTheory.Functor.FullyFaithful -public import Mathlib.CategoryTheory.Monoidal.Braided.Basic public import Mathlib.Data.EReal.Basic public import Mathlib.Tactic public import QuantumInfo.Entropy.VonNeumann -public import QuantumInfo.Entropy.SSA public import QuantumInfo.Entropy.Relative -public import QuantumInfo.Entropy.DPI public import QuantumInfo.Channels.Bundled public import QuantumInfo.Channels.CPTP -public import QuantumInfo.Channels.Dual public import QuantumInfo.Channels.MatrixMap public import QuantumInfo.Channels.Unbundled diff --git a/QuantumInfo/ResourceTheory/HypothesisTesting.lean b/QuantumInfo/ResourceTheory/HypothesisTesting.lean index 88d1d9f432..44a4545309 100644 --- a/QuantumInfo/ResourceTheory/HypothesisTesting.lean +++ b/QuantumInfo/ResourceTheory/HypothesisTesting.lean @@ -6,12 +6,10 @@ Authors: Alex Meiburg, Leonardo A. Lessa, Rodolfo R. Soldati module public import Mathlib.Algebra.Module.Submodule.Lattice -public import Mathlib.Analysis.Subadditive public import Mathlib.CategoryTheory.Functor.FullyFaithful public import Mathlib.CategoryTheory.Monoidal.Braided.Basic public import Mathlib.Data.EReal.Basic public import QuantumInfo.Entropy.VonNeumann -public import QuantumInfo.Entropy.SSA public import QuantumInfo.Entropy.Relative public import QuantumInfo.Entropy.DPI public import QuantumInfo.Channels.Bundled @@ -20,6 +18,8 @@ public import QuantumInfo.Channels.Dual public import QuantumInfo.Channels.MatrixMap public import QuantumInfo.Channels.Unbundled public import QuantumInfo.Measurements.POVM +public import QuantumInfo.ForMathlib.ContinuousSup +public import Mathlib.Topology.Compactification.OnePoint.ProjectiveLine /-! Defines `OptimalHypothesisRate`, the optimal rate of distinguishing an `MState` ρ from a set of other diff --git a/QuantumInfo/ResourceTheory/SteinsLemma.lean b/QuantumInfo/ResourceTheory/SteinsLemma.lean index 0707fc1195..ebc60b2cfb 100644 --- a/QuantumInfo/ResourceTheory/SteinsLemma.lean +++ b/QuantumInfo/ResourceTheory/SteinsLemma.lean @@ -10,6 +10,8 @@ public import QuantumInfo.ForMathlib.HermitianMat.Jordan public import QuantumInfo.ForMathlib.LimSupInf public import QuantumInfo.ResourceTheory.FreeState public import QuantumInfo.ResourceTheory.HypothesisTesting +public import QuantumInfo.ForMathlib.Filter +public import Mathlib.Topology.Algebra.Order.LiminfLimsup @[expose] public section diff --git a/QuantumInfo/States/Ensemble.lean b/QuantumInfo/States/Ensemble.lean index 8a16b6c3e4..5a237dbec6 100644 --- a/QuantumInfo/States/Ensemble.lean +++ b/QuantumInfo/States/Ensemble.lean @@ -6,7 +6,6 @@ Authors: Leonardo A Lessa module public import QuantumInfo.States.Mixed.MState -public import Physlib.Meta.Sorry @[expose] public section diff --git a/QuantumInfo/States/Entanglement.lean b/QuantumInfo/States/Entanglement.lean index b670441d5a..db93a1d1e4 100644 --- a/QuantumInfo/States/Entanglement.lean +++ b/QuantumInfo/States/Entanglement.lean @@ -8,9 +8,6 @@ module public import QuantumInfo.States.Pure.Braket public import QuantumInfo.States.Ensemble public import QuantumInfo.Entropy.VonNeumann -public import QuantumInfo.Entropy.SSA -public import QuantumInfo.Entropy.Relative -public import QuantumInfo.Entropy.DPI public import QuantumInfo.ClassicalInfo.Entropy /-! diff --git a/QuantumInfo/States/Mixed/Fidelity.lean b/QuantumInfo/States/Mixed/Fidelity.lean index 1c7371428c..f502eba83c 100644 --- a/QuantumInfo/States/Mixed/Fidelity.lean +++ b/QuantumInfo/States/Mixed/Fidelity.lean @@ -6,11 +6,9 @@ Authors: Alex Meiburg module public import QuantumInfo.Channels.Bundled -public import QuantumInfo.Channels.CPTP -public import QuantumInfo.Channels.Dual public import QuantumInfo.Channels.MatrixMap public import QuantumInfo.Channels.Unbundled -public import Physlib.Meta.Sorry +public import Physlib.Meta.Linters.Sorry @[expose] public section noncomputable section diff --git a/QuantumInfo/States/Mixed/MState.lean b/QuantumInfo/States/Mixed/MState.lean index 004a282113..bf60579695 100644 --- a/QuantumInfo/States/Mixed/MState.lean +++ b/QuantumInfo/States/Mixed/MState.lean @@ -6,21 +6,17 @@ Authors: Alex Meiburg, Leonardo A. Lessa module public import QuantumInfo.ForMathlib.ContinuousLinearMap -public import QuantumInfo.ForMathlib.ComplexLaplaceTransform -public import QuantumInfo.ForMathlib.ContinuousSup -public import QuantumInfo.ForMathlib.Filter public import QuantumInfo.ForMathlib.HermitianMat public import QuantumInfo.ForMathlib.Isometry public import QuantumInfo.ForMathlib.LinearEquiv public import QuantumInfo.ForMathlib.MatrixNorm.TraceNorm public import QuantumInfo.ForMathlib.Matrix -public import QuantumInfo.ForMathlib.Minimax public import QuantumInfo.ForMathlib.Misc -public import QuantumInfo.ForMathlib.Unitary public import QuantumInfo.ClassicalInfo.Distribution public import QuantumInfo.States.Pure.Braket public import Mathlib.Logic.Equiv.Basic +public import Mathlib.Tactic.LinearCombinationPrime /-! Finite dimensional quantum mixed states, ρ. diff --git a/QuantumInfo/States/Mixed/TraceDistance.lean b/QuantumInfo/States/Mixed/TraceDistance.lean index 93a5439b24..b7e9184aa9 100644 --- a/QuantumInfo/States/Mixed/TraceDistance.lean +++ b/QuantumInfo/States/Mixed/TraceDistance.lean @@ -8,17 +8,12 @@ module public import QuantumInfo.States.Mixed.MState public import QuantumInfo.ForMathlib.ContinuousLinearMap -public import QuantumInfo.ForMathlib.ComplexLaplaceTransform -public import QuantumInfo.ForMathlib.ContinuousSup -public import QuantumInfo.ForMathlib.Filter public import QuantumInfo.ForMathlib.HermitianMat public import QuantumInfo.ForMathlib.Isometry public import QuantumInfo.ForMathlib.LinearEquiv public import QuantumInfo.ForMathlib.MatrixNorm.TraceNorm public import QuantumInfo.ForMathlib.Matrix -public import QuantumInfo.ForMathlib.Minimax public import QuantumInfo.ForMathlib.Misc -public import QuantumInfo.ForMathlib.Unitary @[expose] public section diff --git a/QuantumInfo/States/Pure/Braket.lean b/QuantumInfo/States/Pure/Braket.lean index 99141fc874..0498f0d340 100644 --- a/QuantumInfo/States/Pure/Braket.lean +++ b/QuantumInfo/States/Pure/Braket.lean @@ -6,18 +6,11 @@ Authors: Alex Meiburg, Rodolfo Soldati module public import QuantumInfo.ForMathlib.ContinuousLinearMap -public import QuantumInfo.ForMathlib.ComplexLaplaceTransform -public import QuantumInfo.ForMathlib.ContinuousSup -public import QuantumInfo.ForMathlib.Filter public import QuantumInfo.ForMathlib.HermitianMat public import QuantumInfo.ForMathlib.Isometry public import QuantumInfo.ForMathlib.LinearEquiv -public import QuantumInfo.ForMathlib.MatrixNorm.TraceNorm public import QuantumInfo.ForMathlib.Matrix -public import QuantumInfo.ForMathlib.Minimax public import QuantumInfo.ForMathlib.Misc -public import QuantumInfo.ForMathlib.Unitary -public import QuantumInfo.ClassicalInfo.Distribution /-! Finite dimensional quantum pure states, bra and kets. Mixed states are `MState` in that file. diff --git a/QuantumInfo/States/Pure/Qubit.lean b/QuantumInfo/States/Pure/Qubit.lean index 52d00715b5..0449300b55 100644 --- a/QuantumInfo/States/Pure/Qubit.lean +++ b/QuantumInfo/States/Pure/Qubit.lean @@ -5,12 +5,8 @@ Authors: Alex Meiburg -/ module -public import QuantumInfo.Channels.Bundled -public import QuantumInfo.Channels.CPTP -public import QuantumInfo.Channels.Dual -public import QuantumInfo.Channels.MatrixMap -public import QuantumInfo.Channels.Unbundled public import Physlib.Meta.TODO.Basic +public import QuantumInfo.ForMathlib.HermitianMat.Unitary /-! Quantum theory and operations specific to qubits.