From c1532dd928803793bb63d8d5033177000eeca05f Mon Sep 17 00:00:00 2001 From: Taksh Date: Thu, 16 Jul 2026 17:27:29 +0300 Subject: [PATCH] fix: close Section_4_1 doc comment with -/ instead of --/. Co-authored-by: Cursor --- Analysis/Section_4_1.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_4_1.lean b/Analysis/Section_4_1.lean index 24a11772..4ee438d8 100644 --- a/Analysis/Section_4_1.lean +++ b/Analysis/Section_4_1.lean @@ -302,7 +302,7 @@ theorem Int.neg_one_mul (a:Int) : -1 * a = -a := by sorry /-- Exercise 4.1.8 -/ theorem Int.no_induction : ∃ P: Int → Prop, (P 0 ∧ ∀ n, P n → P (n+1)) ∧ ¬ ∀ n, P n := by sorry -/-- A nonnegative number squared is nonnegative. This is a special case of 4.1.9 that's useful for proving the general case. --/ +/-- A nonnegative number squared is nonnegative. This is a special case of 4.1.9 that's useful for proving the general case. -/ lemma Int.sq_nonneg_of_pos (n:Int) (h: 0 ≤ n) : 0 ≤ n*n := by sorry /-- Exercise 4.1.9. The square of any integer is nonnegative. -/