From 4ec24b6e1c47cacf43b17dbd5390d83f151c9275 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sun, 9 Apr 2023 16:28:55 -0600 Subject: [PATCH] Remove unused imports. --- one-variable-calculus/Apostol/Chapter_I_3_10.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/one-variable-calculus/Apostol/Chapter_I_3_10.lean b/one-variable-calculus/Apostol/Chapter_I_3_10.lean index 494a93b..37a40f0 100644 --- a/one-variable-calculus/Apostol/Chapter_I_3_10.lean +++ b/one-variable-calculus/Apostol/Chapter_I_3_10.lean @@ -1,7 +1,5 @@ import Mathlib.Data.PNat.Basic import Mathlib.Data.Real.Basic -import Mathlib.Order.Basic -import Mathlib.Tactic.LibrarySearch #check Archimedean @@ -57,4 +55,4 @@ theorem pos_imp_exists_pnat_mul_self_geq {x y : ℝ} rw [div_mul, div_self (show x ≠ 0 from LT.lt.ne' hx), div_one] at p' exact ⟨n, p'⟩ -end Real \ No newline at end of file +end Real