instShiftLeft_mathlib — Mathlib

English

`m <<< n` produces the integer obtained by left-shifting the binary representation of m by n places.

Русский

`m <<< n` даёт целое, полученное сдвигом влево числа m на n позиций.

LaTeX

$$$m \\text{ left-shifted by } n$$$

Lean4

/-- `m <<< n` produces an integer whose binary representation
  is obtained by left-shifting the binary representation of `m` by `n` places -/
instance : ShiftLeft ℤ where
  shiftLeft
    | (m : ℕ), (n : ℕ) => Nat.shiftLeft' false m n
    | (m : ℕ), -[n+1] => m >>> (Nat.succ n)
    | -[m+1], (n : ℕ) => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m >>> (Nat.succ n)+1]

Похожие утверждения