diff --git a/Bookshelf/Real/Basic.lean b/Bookshelf/Real/Basic.lean index abec47e..2b2d76d 100644 --- a/Bookshelf/Real/Basic.lean +++ b/Bookshelf/Real/Basic.lean @@ -2,8 +2,6 @@ import Mathlib.Data.Real.Basic notation "ℝ²" => ℝ × ℝ -notation "ℝ³" => ℝ² × ℝ - namespace Real /--