Update src/Init/Data/Nat/Bitwise/Basic.lean

Co-authored-by: Tobias Grosser <[email protected]>
opencompl · Nov 12, 2024 · d9bf86f · d9bf86f
1 parent 7d2bc58
commit d9bf86f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean
@@ -71,7 +71,7 @@ theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
     rw [shiftRight_add, shiftRight_eq_div_pow m k]
     simp [Nat.div_div_eq_div_mul, ← Nat.pow_succ, shiftRight_succ]
 
-theorem shiftRight_eq_zero (m n : Nat) (hn : m < 2 ^n): m >>> n = 0 := by
+theorem shiftRight_eq_zero (m n : Nat) (hn : m < 2^n) : m >>> n = 0 := by
   simp [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt hn]
 
 /-!