Skip to content

Commit a8a24b6

Browse files
fpvandoorndagurtomas
authored andcommitted
fix: move SobolevInequality.lean (#14264)
* Forgot to incorporate 1 review comment from #14165
1 parent 67f763d commit a8a24b6

File tree

2 files changed

+1
-1
lines changed

2 files changed

+1
-1
lines changed

Mathlib.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -1003,6 +1003,7 @@ import Mathlib.Analysis.Fourier.FourierTransformDeriv
10031003
import Mathlib.Analysis.Fourier.Inversion
10041004
import Mathlib.Analysis.Fourier.PoissonSummation
10051005
import Mathlib.Analysis.Fourier.RiemannLebesgueLemma
1006+
import Mathlib.Analysis.FunctionalSpaces.SobolevInequality
10061007
import Mathlib.Analysis.Hofer
10071008
import Mathlib.Analysis.InnerProductSpace.Adjoint
10081009
import Mathlib.Analysis.InnerProductSpace.Basic
@@ -3054,7 +3055,6 @@ import Mathlib.MeasureTheory.Integral.Pi
30543055
import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani
30553056
import Mathlib.MeasureTheory.Integral.SetIntegral
30563057
import Mathlib.MeasureTheory.Integral.SetToL1
3057-
import Mathlib.MeasureTheory.Integral.SobolevInequality
30583058
import Mathlib.MeasureTheory.Integral.TorusIntegral
30593059
import Mathlib.MeasureTheory.Integral.VitaliCaratheodory
30603060
import Mathlib.MeasureTheory.MeasurableSpace.Basic

0 commit comments

Comments
 (0)