diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 61e68c58cbc9..f0c6355dd742 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1312,6 +1312,34 @@ theorem umod_eq {x y : BitVec n} :
 theorem toNat_umod {x y : BitVec n} :
     (x.umod y).toNat = x.toNat % y.toNat := rfl
 
+/-! ### sdiv -/
+
+/-- Equation theorem for `sdiv` in terms of `udiv` -/
+theorem sdiv_eq (x y : BitVec w) : x.sdiv y =
+  match x.msb, y.msb with
+  | false, false => udiv x y
+  | false, true  =>  - (x.udiv (- y))
+  | true,  false => - ((- x).udiv y)
+  | true,  true  => (- x).udiv (- y) := by
+  rw [BitVec.sdiv]
+  rcases x.msb <;> rcases y.msb <;> simp [BitVec.sdiv]
+
+/-! ### smod -/
+
+/-- Equation theorem for `smod` in terms of `umod` -/
+theorem smod_eq (x y : BitVec w) : x.smod y =
+  match x.msb, y.msb with
+  | false, false => x.umod y
+  | false, true =>
+    let u := x.umod (- y)
+    (if u = 0#w then u else u + y)
+  | true, false =>
+    let u := umod (.neg x) y
+    (if u = 0#w then u else y - u)
+  | true, true => - ((- x).umod (- y)) := by
+  simp [BitVec.smod]
+  rcases x.msb <;> rcases y.msb <;> simp
+
 /-! ### signExtend -/
 
 /-- Equation theorem for `Int.sub` when both arguments are `Int.ofNat` -/