chore: remove ToMathlib/Height, which has been upstreamed (#186)

Possibly, more material (e.g. in MinLayer) can be removed now; I did not scrutinise this extremely carefully. Co-authored-by: Pietro Monticone <[email protected]>
fpvandoorn · Nov 22, 2024 · 1b5b0d0 · 1b5b0d0
1 parent fec289d
commit 1b5b0d0
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 359 deletions.
diff --git a/Carleson.lean b/Carleson.lean
@@ -39,7 +39,6 @@ import Carleson.Psi
 import Carleson.RealInterpolation
 import Carleson.TileExistence
 import Carleson.TileStructure
-import Carleson.ToMathlib.Height
 import Carleson.ToMathlib.MeasureReal
 import Carleson.ToMathlib.MinLayer
 import Carleson.ToMathlib.Misc

diff --git a/Carleson/ToMathlib/Height.lean b/Carleson/ToMathlib/Height.lean