diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index e3b07535c6a1..6b9727203f10 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -714,10 +714,16 @@ instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_com
   ext i
   simp
 
+instance : Std.IdempotentOp (α := BitVec n) (· ||| · ) where
+  idempotent _ := BitVec.or_self
+
 @[simp] theorem or_zero {x : BitVec w} : x ||| 0#w = x := by
   ext i
   simp
 
+instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
+  right_id _ := BitVec.or_zero
+
 @[simp] theorem zero_or {x : BitVec w} : 0#w ||| x = x := by
   ext i
   simp
@@ -775,6 +781,9 @@ instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_co
   ext i
   simp
 
+instance : Std.IdempotentOp (α := BitVec n) (· &&& · ) where
+  idempotent _ := BitVec.and_self
+
 @[simp] theorem and_zero {x : BitVec w} : x &&& 0#w = 0#w := by
   ext i
   simp
@@ -787,6 +796,9 @@ instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_co
   ext i
   simp
 
+instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) where
+  right_id _ := BitVec.and_allOnes
+
 @[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
   ext i
   simp
@@ -843,6 +855,9 @@ instance : Std.Commutative (fun (x y : BitVec w) => x ^^^ y) := ⟨BitVec.xor_co
   ext i
   simp
 
+instance : Std.LawfulCommIdentity (α := BitVec n) (· ^^^ · ) (0#n) where
+  right_id _ := BitVec.xor_zero
+
 @[simp] theorem zero_xor {x : BitVec w} : 0#w ^^^ x = x := by
   ext i
   simp