tonat thms

leanprover · Dec 9, 2024 · 7aedee4 · 7aedee4
1 parent 4f21275
commit 7aedee4
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -3036,7 +3036,6 @@ theorem toNat_rotateRight {x : BitVec w} {r : Nat} :
     (x.rotateRight r).toNat = (x.toNat >>> (r % w)) ||| x.toNat <<< (w - r % w) % (2^w) := by
   simp only [rotateRight, rotateRightAux, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
 
-
 /- ## twoPow -/
 
 theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by