source
theorem Int.shiftRight_eq (n : Int) (s : Nat) :
n >>> s = n.shiftRight s
source
@[simp]
theorem Int.natCast_shiftRight (n s : Nat) :
↑(n >>> s) = ↑n >>> s
source
@[simp]
theorem Int.negSucc_shiftRight (m n : Nat) :
negSucc m >>> n = negSucc (m >>> n)
source
theorem Int.shiftRight_add (i : Int) (m n : Nat) :
i >>> (m + n) = i >>> m >>> n
source
theorem Int.shiftRight_eq_div_pow (m : Int) (n : Nat) :
m >>> n = m / ↑(2 ^ n)
source
@[simp]
theorem Int.zero_shiftRight (n : Nat) :
0 >>> n = 0
source
@[simp]
theorem Int.shiftRight_zero (n : Int) :
n >>> 0 = n
source
theorem Int.le_shiftRight_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) :
n ≤ n >>> s
source
theorem Int.shiftRight_le_of_nonneg {n : Int} {s : Nat} (h : 0 ≤ n) :
n >>> s ≤ n
source
theorem Int.le_shiftRight_of_nonneg {n : Int} {s : Nat} (h : 0 ≤ n) :
0 ≤ n >>> s
source
theorem Int.shiftRight_le_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) :
n >>> s ≤ 0
source
@[simp]
theorem Int.natCast_shiftLeft (n s : Nat) :
↑(n <<< s) = ↑n <<< s
source
@[simp]
theorem Int.zero_shiftLeft (n : Nat) :
0 <<< n = 0
source
@[simp]
theorem Int.shiftLeft_zero (n : Int) :
n <<< 0 = n
source
theorem Int.shiftLeft_succ (m : Int) (n : Nat) :
m <<< (n + 1) = m <<< n * 2
source
theorem Int.shiftLeft_succ' (m : Int) (n : Nat) :
m <<< (n + 1) = 2 * m <<< n
source
theorem Int.shiftLeft_eq (a : Int) (b : Nat) :
a <<< b = a * 2 ^ b
source
theorem Int.shiftLeft_eq' (a : Int) (b : Nat) :
a <<< b = a * ↑(2 ^ b)
source
theorem Int.shiftLeft_add (a : Int) (b c : Nat) :
a <<< (b + c) = a <<< b <<< c
source
@[simp]
theorem Int.shiftLeft_shiftRight_cancel (a : Int) (b : Nat) :
a <<< b >>> b = a
source
theorem Int.shiftLeft_shiftRight_eq_shiftLeft_of_le {b c : Nat} (h : c ≤ b) (a : Int) :
a <<< b >>> c = a <<< (b - c)
source
theorem Int.shiftLeft_shiftRight_eq_shiftRight_of_le {b c : Nat} (h : b ≤ c) (a : Int) :
a <<< b >>> c = a >>> (c - b)
source
theorem Int.shiftLeft_shiftRight_eq (a : Int) (b c : Nat) :
a <<< b >>> c = a <<< (b - c) >>> (c - b)
source
@[simp]
theorem Int.shiftRight_shiftLeft_cancel {a : Int} {b : Nat} (h : 2 ^ b ∣ a) :
a >>> b <<< b = a
source
theorem Int.add_shiftLeft (a b : Int) (n : Nat) :
(a + b) <<< n = a <<< n + b <<< n
source
theorem Int.neg_shiftLeft (a : Int) (n : Nat) :
(-a) <<< n = -a <<< n
source
theorem Int.shiftLeft_mul (a b : Int) (n : Nat) :
a <<< n * b = (a * b) <<< n
source
theorem Int.mul_shiftLeft (a b : Int) (n : Nat) :
a * b <<< n = (a * b) <<< n
source
theorem Int.shiftLeft_mul_shiftLeft (a b : Int) (m n : Nat) :
a <<< m * b <<< n = (a * b) <<< (m + n)
source
@[simp]
theorem Int.shiftLeft_eq_zero_iff {a : Int} {n : Nat} :
a <<< n = 0 ↔ a = 0
source
instance Int.instNeZeroHShiftLeftNat {a : Int} {n : Nat} [NeZero a] :
NeZero (a <<< n)