diff --git a/Batteries.lean b/Batteries.lean
index 3c49850ed8..6934764076 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -16,6 +16,7 @@ import Batteries.Data.Array
 import Batteries.Data.AssocList
 import Batteries.Data.BinaryHeap
 import Batteries.Data.BinomialHeap
+import Batteries.Data.BitVec
 import Batteries.Data.ByteArray
 import Batteries.Data.ByteSubarray
 import Batteries.Data.Char
diff --git a/Batteries/Data/BitVec.lean b/Batteries/Data/BitVec.lean
new file mode 100644
index 0000000000..39bac8df96
--- /dev/null
+++ b/Batteries/Data/BitVec.lean
@@ -0,0 +1 @@
+import Batteries.Data.BitVec.GF2
diff --git a/Batteries/Data/BitVec/GF2.lean b/Batteries/Data/BitVec/GF2.lean
new file mode 100644
index 0000000000..0ca8b62709
--- /dev/null
+++ b/Batteries/Data/BitVec/GF2.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2024 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+namespace BitVec.GF2
+
+/--
+Modular multplication of polynomials over the two-element field GF(2).
+
+The modulus is the polynomial of degree `d` whose coefficients other than the leading `1` are
+encoded by the bitvector `m`; `x` and `y` encode the two multiplicands, polynomials of degree less
+than `d`.
+-/
+def mulMod (x y m : BitVec d) : BitVec d :=
+  if d = 0 then 0 else Id.run do
+    let mut x : BitVec d := x
+    let mut r : BitVec d := 0
+    for i in [:d-1] do
+      r := bif y[i]! then r ^^^ x else r
+      x := bif x.msb then x <<< 1 ^^^ m else x <<< 1
+    r := bif y[d-1]! then r ^^^ x else r
+    return r
+
+/--
+Modular exponentiation of polynomials over the two-element field GF(2).
+
+The modulus is the polynomial of degree `d` whose coefficients other than the leading `1` are
+encoded by the bitvector `m`; `x` encodes the base, a polynomial of degree less than `d`.
+-/
+def powMod (x : BitVec d) (n : Nat) (m : BitVec d) : BitVec d :=
+  if d = 0 then 0 else Id.run do
+    let mut n := n
+    let mut x : BitVec d := x
+    let mut r : BitVec d := 1
+    while n > 1 do
+      r := if n % 2 = 1 then mulMod r x m else r
+      x := mulMod x x m
+      n := n >>> 1
+    r := if n = 1 then mulMod r x m else r
+    return r