diff --git a/Analysis/Section_4_1.lean b/Analysis/Section_4_1.lean
index 24a11772..5985414a 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 14f57bb5..f45e0089 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