instShiftRight_mathlib

Mathlib.Data.Int.Bitwise

URI: https://scilib.ai/kg/mathlib#Int.instShiftRight_mathlib

← MathLib Explorer

English

`m >>> n` equals `m <<< (-n)`; right-shift by n equals left-shift by -n.

Русский

`m >>> n` эквивалентно `m <<< (-n)`; сдвиг вправо на n равен сдвигу влево на -n.

LaTeX

$$$m >>> n = m <<< (-n)$$$

Lean4

/-- `m >>> n` produces an integer whose binary representation
  is obtained by right-shifting the binary representation of `m` by `n` places -/
instance : ShiftRight ℤ where shiftRight m n := m <<< (-n)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru