diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 36ac357b1c..4566aa60e8 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -1,7 +1,10 @@ import LeanAPAP.Extras.BSG import LeanAPAP.FiniteField.Basic +import LeanAPAP.Mathlib.Algebra.Algebra.Rat import LeanAPAP.Mathlib.Algebra.Group.AddChar import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic +import LeanAPAP.Mathlib.Algebra.Star.Basic +import LeanAPAP.Mathlib.Algebra.Star.Rat import LeanAPAP.Mathlib.Analysis.RCLike.Basic import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean index 1bd2e98203..19b6e391ab 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean @@ -1,6 +1,5 @@ import LeanAPAP.Mathlib.Analysis.RCLike.Basic import LeanAPAP.Mathlib.Data.Fintype.Order -import LeanAPAP.Mathlib.Data.NNReal.Basic import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef import LeanAPAP.Mathlib.Order.Filter.Basic diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean index ef78924492..c4b588ed1b 100644 --- a/LeanAPAP/Prereqs/NNLpNorm.lean +++ b/LeanAPAP/Prereqs/NNLpNorm.lean @@ -1,8 +1,6 @@ import Mathlib.Analysis.Normed.Group.Constructions import Mathlib.MeasureTheory.Integral.Bochner import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal -import LeanAPAP.Mathlib.Data.ENNReal.Basic -import LeanAPAP.Mathlib.Data.ENNReal.Operations import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic import LeanAPAP.Prereqs.Expect.Basic