refactor: More redundant imports

2024-12-20 16:53:14 +00:00 · 2024-12-20 16:53:14 +00:00 · 14677e6332
commit 14677e6332
parent f3cb311028
30 changed files with 0 additions and 76 deletions
--- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@ -3,10 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.PureU1.Sorts
 import HepLean.AnomalyCancellation.PureU1.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.VectorLike
-import Mathlib.Logic.Equiv.Fin
 /-!
 # Basis of `LinSols` in the even case

--- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
@ -3,13 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.PureU1.Basic
-import HepLean.AnomalyCancellation.PureU1.ConstAbs
 import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
-import HepLean.AnomalyCancellation.PureU1.Permutations
-import Mathlib.RepresentationTheory.Basic
-import Mathlib.Tactic.Polyrith
 /-!

 # Line In Cubic Even case
--- a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
@ -3,14 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.PureU1.Basic
-import HepLean.AnomalyCancellation.PureU1.ConstAbs
-import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
-import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.Even.LineInCubic
-import HepLean.AnomalyCancellation.PureU1.Permutations
-import Mathlib.RepresentationTheory.Basic
-import Mathlib.Tactic.Polyrith
 /-!
 # Parameterization in even case

--- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
@ -4,11 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.PureU1.Basic
-import HepLean.AnomalyCancellation.PureU1.Permutations
-import HepLean.AnomalyCancellation.PureU1.VectorLike
 import HepLean.AnomalyCancellation.PureU1.ConstAbs
-import Mathlib.Tactic.Polyrith
-import Mathlib.RepresentationTheory.Basic
 /-!
 # Line in plane condition

--- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@ -3,10 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.PureU1.Sorts
 import HepLean.AnomalyCancellation.PureU1.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.VectorLike
-import Mathlib.Logic.Equiv.Fin
 /-!
 # Basis of `LinSols` in the odd case

--- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
@ -3,14 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.PureU1.Basic
-import HepLean.AnomalyCancellation.PureU1.Permutations
-import HepLean.AnomalyCancellation.PureU1.VectorLike
-import HepLean.AnomalyCancellation.PureU1.ConstAbs
 import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
 import HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear
-import Mathlib.Tactic.Polyrith
-import Mathlib.RepresentationTheory.Basic
 /-!

 # Line In Cubic Odd case
--- a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
@ -3,14 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.PureU1.Basic
-import HepLean.AnomalyCancellation.PureU1.Permutations
-import HepLean.AnomalyCancellation.PureU1.VectorLike
-import HepLean.AnomalyCancellation.PureU1.ConstAbs
-import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
 import HepLean.AnomalyCancellation.PureU1.Odd.LineInCubic
-import Mathlib.Tactic.Polyrith
-import Mathlib.RepresentationTheory.Basic
 /-!
 # Parameterization in odd case

--- a/HepLean/AnomalyCancellation/PureU1/Permutations.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
@ -5,8 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.PureU1.Basic
 import HepLean.AnomalyCancellation.GroupActions
-import Mathlib.Tactic.Polyrith
-import Mathlib.RepresentationTheory.Basic
 /-!
 # Permutations of Pure U(1) ACC

--- a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
+++ b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.PureU1.Sorts
-import Mathlib.Logic.Equiv.Fin
 /-!
 # Vector like charges

--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/Basic.lean
@ -3,13 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import Mathlib.Tactic.FinCases
-import Mathlib.Algebra.Module.Basic
 import Mathlib.Tactic.Ring
-import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import HepLean.AnomalyCancellation.Basic
-import Mathlib.Algebra.BigOperators.Fin
-import Mathlib.Logic.Equiv.Fin
 /-!
 # Anomaly cancellation conditions for n family SM.

--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
@ -3,10 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.SM.Basic
-import HepLean.AnomalyCancellation.SM.NoGrav.Basic
 import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
-import Mathlib.NumberTheory.FLT.Three
 /-!
 # Lemmas for 1 family SM Accs

--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@ -3,12 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.SM.Basic
 import HepLean.AnomalyCancellation.SM.NoGrav.Basic
-import Mathlib.Tactic.FieldSimp
-import Mathlib.Tactic.Linarith
-import Mathlib.NumberTheory.FLT.Basic
-import Mathlib.Algebra.QuadraticDiscriminant
 import Mathlib.NumberTheory.FLT.Three
 /-!
 # Parameterizations for solutions to the linear ACCs for 1 family
--- a/HepLean/AnomalyCancellation/SM/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SM/Permutations.lean
@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SM.Basic
-import Mathlib.Tactic.Polyrith
 import Mathlib.RepresentationTheory.Basic
 /-!

--- a/HepLean/AnomalyCancellation/SMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Basic.lean
@ -3,13 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import Mathlib.Tactic.FinCases
-import Mathlib.Algebra.Module.Basic
-import Mathlib.Tactic.Ring
-import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import HepLean.AnomalyCancellation.Basic
-import Mathlib.Algebra.BigOperators.Fin
-import Mathlib.Logic.Equiv.Fin
 /-!
 # Anomaly cancellation conditions for n family SM.
 -/
--- a/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.Permutations
 import HepLean.AnomalyCancellation.GroupActions
 /-!
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.Permutations
 import HepLean.AnomalyCancellation.GroupActions
 /-!
--- a/HepLean/AnomalyCancellation/SMNu/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Permutations.lean
@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SMNu.Basic
-import Mathlib.Tactic.Polyrith
 import Mathlib.RepresentationTheory.Basic
 /-!
 # Permutations of SM charges with RHN.
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
 import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
 /-!
 # B Minus L in SM with RHN.
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.Permutations
 import HepLean.AnomalyCancellation.GroupActions
 /-!
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
 import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
 /-!
 # Bound on plane dimension
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
 import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
 /-!
 # Hypercharge in SM with RHN.
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
 import HepLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
 /-!
 # Solutions from quad solutions
--- a/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.StandardModel.Basic
-import HepLean.Meta.Informal.Basic
 /-!

 # The Georgi-Glashow Model
--- a/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean
@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.StandardModel.Basic
-import HepLean.Meta.Informal.Basic
 /-!

 # The Pati-Salam Model
--- a/HepLean/BeyondTheStandardModel/Spin10/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/Spin10/Basic.lean
@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.BeyondTheStandardModel.PatiSalam.Basic
 import HepLean.BeyondTheStandardModel.GeorgiGlashow.Basic
-import HepLean.Meta.Informal.Basic
 /-!

 # The Spin(10) Model
--- a/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
+++ b/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
@ -7,7 +7,6 @@ import HepLean.BeyondTheStandardModel.TwoHDM.Basic
 import HepLean.StandardModel.HiggsBoson.GaugeAction
 import Mathlib.LinearAlgebra.Matrix.PosDef
 import Mathlib.Analysis.CStarAlgebra.Matrix
-import Mathlib.Analysis.Matrix
 /-!

 # Gauge orbits for the 2HDM
--- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
@ -3,9 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Rows
-import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 /-!
 # Relations for the CKM Matrix

--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
@ -3,10 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Rows
 import HepLean.FlavorPhysics.CKMMatrix.Invariants
-import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 /-!
 # Standard parameterization for the CKM Matrix

--- a/HepLean/Meta/Notes/HTMLNote.lean
+++ b/HepLean/Meta/Notes/HTMLNote.lean
@ -4,7 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Meta.Notes.NoteFile
-import HepLean.Meta.Basic
 import HepLean.Meta.Informal.Post
 /-!

--- a/HepLean/PerturbationTheory/Wick/KoszulOrder.lean
+++ b/HepLean/PerturbationTheory/Wick/KoszulOrder.lean
@ -3,9 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import Mathlib.Algebra.FreeAlgebra
-import Mathlib.Algebra.Lie.OfAssociative
-import Mathlib.Analysis.Complex.Basic
 import HepLean.PerturbationTheory.Wick.Signs.StaticWickCoef
 /-!