Update src/Init/Data/BitVec/Lemmas.lean

Co-authored-by: Siddharth <[email protected]>
leanprover · Oct 10, 2024 · c847376 · c847376
1 parent 9745eee
commit c847376
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -961,7 +961,7 @@ theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
   ext i
   simp
 
-theorem not_eq_iff_eq_not {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
+theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
   constructor
   · intro h
     rw [← h]