From c12b1d0a55371935980fe4598769ad4d119cd193 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Tue, 14 Jan 2025 10:56:48 +0000
Subject: [PATCH] chore: fix docstring in `Bitvec.toNat_add_of_lt` (#6638)

This PR correct the docstring of theorem `Bitvec.toNat_add_of_lt`
---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 377ab5cc885f..7387c02591e7 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3539,7 +3539,7 @@ theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) :=
 
 /-! ### Non-overflow theorems -/
 
-/-- If `x.toNat * y.toNat < 2^w`, then the multiplication `(x * y)` does not overflow. -/
+/-- If `x.toNat + y.toNat < 2^w`, then the addition `(x + y)` does not overflow. -/
 theorem toNat_add_of_lt {w} {x y : BitVec w} (h : x.toNat + y.toNat < 2^w) :
     (x + y).toNat = x.toNat + y.toNat := by
   rw [BitVec.toNat_add, Nat.mod_eq_of_lt h]