Skip to content

Commit 1513ca0

Browse files
chore: remove dead code
The lemmas are being upstreamed in leanprover-community/mathlib4#31318 and leanprover-community/mathlib4#31320.
1 parent e669b9d commit 1513ca0

File tree

4 files changed

+0
-39
lines changed

4 files changed

+0
-39
lines changed

Carleson.lean

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -47,10 +47,7 @@ import Carleson.ProofData
4747
import Carleson.Psi
4848
import Carleson.TileExistence
4949
import Carleson.TileStructure
50-
import Carleson.ToMathlib.Analysis.Convex.SpecificFunctions.Basic
5150
import Carleson.ToMathlib.Analysis.Convolution
52-
import Carleson.ToMathlib.Analysis.Normed.Group.Basic
53-
import Carleson.ToMathlib.Analysis.SpecialFunctions.Pow.Deriv
5451
import Carleson.ToMathlib.Annulus
5552
import Carleson.ToMathlib.BoundedCompactSupport
5653
import Carleson.ToMathlib.BoundedFiniteSupport

Carleson/ToMathlib/Analysis/Convex/SpecificFunctions/Basic.lean

Lines changed: 0 additions & 7 deletions
This file was deleted.

Carleson/ToMathlib/Analysis/Normed/Group/Basic.lean

Lines changed: 0 additions & 21 deletions
This file was deleted.

Carleson/ToMathlib/Analysis/SpecialFunctions/Pow/Deriv.lean

Lines changed: 0 additions & 8 deletions
This file was deleted.

0 commit comments

Comments
 (0)