From 2fc3c191cf9776cd47bfb064c70c6878bb08718e Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 15 Jul 2026 11:28:27 +0300 Subject: [PATCH] fix: disambiguate duplicate "Definition of subtraction" labels Int and Rat sections shared the same Verso doc label. Co-authored-by: Cursor --- Analysis/Section_4_1.lean | 2 +- Analysis/Section_4_2.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Analysis/Section_4_1.lean b/Analysis/Section_4_1.lean index 24a117726..5985414a5 100644 --- a/Analysis/Section_4_1.lean +++ b/Analysis/Section_4_1.lean @@ -215,7 +215,7 @@ instance Int.instCommRing : CommRing Int where zero_mul := by sorry mul_zero := by sorry -/-- Definition of subtraction -/ +/-- Definition of subtraction (integers). -/ theorem Int.sub_eq (a b:Int) : a - b = a + (-b) := by rfl theorem Int.sub_eq_formal_sub (a b:ℕ) : (a:Int) - (b:Int) = a —— b := by sorry diff --git a/Analysis/Section_4_2.lean b/Analysis/Section_4_2.lean index 14f57bb5f..f45e00897 100644 --- a/Analysis/Section_4_2.lean +++ b/Analysis/Section_4_2.lean @@ -237,7 +237,7 @@ instance Rat.instField : Field Rat where example : (3//4) / (5//6) = 9 // 10 := by sorry -/-- Definition of subtraction -/ +/-- Definition of subtraction (rationals). -/ theorem Rat.sub_eq (a b:Rat) : a - b = a + (-b) := by rfl def Rat.coe_int_hom : ℤ →+* Rat where