instHShiftLeftNat — Mathlib

English

There is a left-shift operation on numbers defined by the function shiftl; it provides a natural way to shift the binary representation of a number to the left by a given number of positions.

Русский

Существует операция левый сдвиг для чисел, определённая функцией shiftl; она задаёт сдвиг двоичного представления числа влево на заданное число позиций.

LaTeX

$$$hShiftLeft = Num.shiftl$$$

Lean4

instance : HShiftLeft Num Nat Num where hShiftLeft := Num.shiftl

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