From d9bf86f52686650365f5c465fc5f8619d8f1c9d7 Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Tue, 12 Nov 2024 12:33:50 -0800 Subject: [PATCH] Update src/Init/Data/Nat/Bitwise/Basic.lean Co-authored-by: Tobias Grosser --- src/Init/Data/Nat/Bitwise/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean index 963b19ac1140..edc8d67656aa 100644 --- 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] /-!