Skip to content

Commit 6d1c5f5

Browse files
chore: remove deprecated modules (#504)
I'd meant to remove these after finishing the mathlib bump, but I forgot. I don't think they really serve a purpose here.
1 parent 98085ac commit 6d1c5f5

File tree

3 files changed

+0
-15
lines changed

3 files changed

+0
-15
lines changed

Carleson.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -77,8 +77,6 @@ import Carleson.ToMathlib.MeasureTheory.Measure.Haar.Unique
7777
import Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling
7878
import Carleson.ToMathlib.MeasureTheory.Measure.NNReal
7979
import Carleson.ToMathlib.MeasureTheory.Measure.Prod
80-
import Carleson.ToMathlib.MeasureTheory.Measure.Restrict
81-
import Carleson.ToMathlib.MeasureTheory.Measure.SumRestrict
8280
import Carleson.ToMathlib.MinLayer
8381
import Carleson.ToMathlib.Misc
8482
import Carleson.ToMathlib.Order.Chain

Carleson/ToMathlib/MeasureTheory/Measure/Restrict.lean

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

Carleson/ToMathlib/MeasureTheory/Measure/SumRestrict.lean

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

0 commit comments

Comments
 (0)