diff --git a/HepLean.lean b/HepLean.lean index ee22052..5cbd5d9 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -1,6 +1,5 @@ import HepLean.AnomalyCancellation.Basic import HepLean.AnomalyCancellation.GroupActions -import HepLean.AnomalyCancellation.LinearMaps import HepLean.AnomalyCancellation.MSSMNu.B3 import HepLean.AnomalyCancellation.MSSMNu.Basic import HepLean.AnomalyCancellation.MSSMNu.HyperCharge @@ -59,7 +58,8 @@ import HepLean.FlavorPhysics.CKMMatrix.Relations import HepLean.FlavorPhysics.CKMMatrix.Rows import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters -import HepLean.GroupTheory.SO3.Basic +import HepLean.Mathematics.SO3.Basic +import HepLean.Mathematics.LinearMaps import HepLean.SpaceTime.AsSelfAdjointMatrix import HepLean.SpaceTime.Basic import HepLean.SpaceTime.CliffordAlgebra diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean index 9014d50..c44b98f 100644 --- a/HepLean/AnomalyCancellation/Basic.lean +++ b/HepLean/AnomalyCancellation/Basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import HepLean.AnomalyCancellation.LinearMaps +import HepLean.Mathematics.LinearMaps import Mathlib.Algebra.Module.Basic import Mathlib.LinearAlgebra.FiniteDimensional /-! diff --git a/HepLean/AnomalyCancellation/LinearMaps.lean b/HepLean/Mathematics/LinearMaps.lean similarity index 100% rename from HepLean/AnomalyCancellation/LinearMaps.lean rename to HepLean/Mathematics/LinearMaps.lean diff --git a/HepLean/GroupTheory/SO3/Basic.lean b/HepLean/Mathematics/SO3/Basic.lean similarity index 100% rename from HepLean/GroupTheory/SO3/Basic.lean rename to HepLean/Mathematics/SO3/Basic.lean diff --git a/HepLean/SpaceTime/LorentzGroup/Rotations.lean b/HepLean/SpaceTime/LorentzGroup/Rotations.lean index c4a861d..605d025 100644 --- a/HepLean/SpaceTime/LorentzGroup/Rotations.lean +++ b/HepLean/SpaceTime/LorentzGroup/Rotations.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.LorentzGroup.Basic -import HepLean.GroupTheory.SO3.Basic +import HepLean.Mathematics.SO3.Basic import Mathlib.Topology.Constructions /-! # Rotations