chore: fix docstring in Bitvec.toNat_add_of_lt (#6638)

This PR correct the docstring of theorem `Bitvec.toNat_add_of_lt`
leanprover · Jan 14, 2025 · c12b1d0 · c12b1d0
1 parent 85294b8
commit c12b1d0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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]