diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index a57654a9a535e..9d6e7dce59c22 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1061,7 +1061,6 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
 @[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
     BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
 
--- deprecate?
 @[simp]
 theorem shiftLeft_zero (x : BitVec w) : x <<< 0 = x := by
   apply eq_of_toNat_eq
@@ -3193,4 +3192,10 @@ abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLs
 @[deprecated msb_sshiftRight (since := "2024-10-03")]
 abbrev sshiftRight_msb_eq_msb := @msb_sshiftRight
 
+@[deprecated shiftLeft_zero (since := "2024-10-27")]
+abbrev shiftLeft_zero_eq := @shiftLeft_zero
+
+@[deprecated ushiftRight_zero (since := "2024-10-27")]
+abbrev ushiftRight_zero_eq := @ushiftRight_zero
+
 end BitVec