Nat.shiftRight_eq_div_pow
theorem Nat.shiftRight_eq_div_pow : ∀ (m n : ℕ), m >>> n = m / 2 ^ n
This theorem states that for any two natural numbers `m` and `n`, the operation of right bitwise shift of `m` by `n` places is equal to the operation of integer division of `m` by `2` to the power of `n`. Bitwise shift to the right effectively divides the number by 2 for each shift, hence the equivalence to dividing by `2^n`.
More concisely: For all natural numbers m and n, m >> n = m / (2^n), where >> denotes right bitwise shift and / denotes integer division.
|
Nat.shiftLeft_eq
theorem Nat.shiftLeft_eq : ∀ (a b : ℕ), a <<< b = a * 2 ^ b
This theorem states that for all natural numbers 'a' and 'b', the operation of shifting 'a' to the left by 'b' places is equivalent to multiplying 'a' by 2 to the power of 'b'. In other words, in the domain of natural numbers, the left shift operation is the same as multiplication by a power of 2.
More concisely: For all natural numbers a and b, shifting a left by b places is equivalent to multiplying a by 2 raised to the power of b.
|
Nat.shiftRight_add
theorem Nat.shiftRight_add : ∀ (m n k : ℕ), m >>> (n + k) = m >>> n >>> k
This theorem states that for all natural numbers `m`, `n`, and `k`, the shift-right operation on `m` by the sum of `n` and `k` is equivalent to performing a shift-right operation on `m` by `n`, and then performing another shift-right operation on the result by `k`. The shift-right operation, denoted by `>>>`, shifts the binary representation of a number to the right, effectively dividing the number by a power of 2.
More concisely: For all natural numbers m, n, and k, (m >>> (n + k)) is equivalent to (m >>> n) >>> k.
|