diff --git a/Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean b/Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean
index 0755653904..8a890c9f11 100644
--- a/Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean
+++ b/Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean
@@ -77,12 +77,6 @@ theorem repr_fieldOfBits (B : Basis (Fin n) (ZMod 2) F) (a : List Bool) (u : Fin
 theorem fieldOfBits_nil (B : Basis (Fin n) (ZMod 2) F) : fieldOfBits B [] = 0 := by
   simp [fieldOfBits]
 
-theorem bitEquiv_symm_foldl_xor (l : List Bool) :
-    bitEquiv.symm (l.foldl xor false) = (l.map bitEquiv.symm).sum := by
-  rw [← map_list_sum]
-  congr 1
-  simp [List.sum_eq_foldl, Bool.add_eq_xor, Bool.zero_eq_false]
-
 /-- The coordinates of a sum: `listXor` adds coordinate words. -/
 theorem fieldOfBits_listXor (B : Basis (Fin n) (ZMod 2) F) (words : List (List Bool)) :
     fieldOfBits B (listXor n words) = (words.map (fieldOfBits B)).sum := by
diff --git a/Complexity/Foundations/Data/BitString/ZModTwo.lean b/Complexity/Foundations/Data/BitString/ZModTwo.lean
index a533aaf9aa..dbc9f97352 100644
--- a/Complexity/Foundations/Data/BitString/ZModTwo.lean
+++ b/Complexity/Foundations/Data/BitString/ZModTwo.lean
@@ -30,6 +30,7 @@ identifies `ZMod 2` with `Bool`; it equals Mathlib's `ZMod.ringEquivOfPrime`
 * `Cslib.BitString.bitEquiv_eq_ringEquivOfPrime`: `bitEquiv` is `ZMod.ringEquivOfPrime Bool`.
 * `Cslib.BitString.bitEquiv_symm_apply`, `Cslib.BitString.bitEquiv_symm_false`,
   `Cslib.BitString.bitEquiv_symm_true`: `bitEquiv.symm` reads `false` as `0` and `true` as `1`.
+* `Cslib.BitString.bitEquiv_symm_foldl_xor`: `bitEquiv.symm` turns a fold over `xor` into a sum.
 
 ## References
 
@@ -67,4 +68,11 @@ theorem bitEquiv_symm_false : bitEquiv.symm false = 0 := rfl
 @[simp]
 theorem bitEquiv_symm_true : bitEquiv.symm true = 1 := rfl
 
+/-- The inverse ring isomorphism maps a fold over `xor` to the sum of the mapped bits. -/
+theorem bitEquiv_symm_foldl_xor (l : List Bool) :
+    bitEquiv.symm (l.foldl xor false) = (l.map bitEquiv.symm).sum := by
+  rw [← map_list_sum]
+  congr 1
+  simp [List.sum_eq_foldl, Bool.add_eq_xor, Bool.zero_eq_false]
+
 end Cslib.BitString