generated by GitHub Action

yuma-mizuno · Jun 23, 2024 · b210de9 · b210de9
1 parent b6026f9
commit b210de9
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/Tutorial/Advanced/Analysis/Lecture1.lean b/Tutorial/Advanced/Analysis/Lecture1.lean
@@ -265,8 +265,6 @@ theorem HasDerivAt.mul {f : ℝ → ℝ} (hf : HasDerivAt f f' a) (hg : HasDeriv
     case eq4 =>
       sorry
 
--- 次の問題で使うかも？
-#check Nat.succ_eq_add_one
 
 /-- 単項式の微分 -/
 theorem hasDerivAt_pow (n : ℕ) (a : ℝ) :

diff --git a/Tutorial/Basic/Lecture1.lean b/Tutorial/Basic/Lecture1.lean
@@ -1,4 +1,4 @@
-import Std
+import Batteries
 
 /- # 遊び方 -/