shiftRight_one

Mathlib.Data.Nat.BinaryRec

URI: https://scilib.ai/kg/mathlib#Nat.shiftRight_one

English

Shifting a natural number right by one equals division by two.

Русский

Сдвиг вправо на единицу эквивалентен делению на два (получаем целочисленное деление).

LaTeX

$$$n \ggg 1 = \dfrac{n}{2}$$$

Lean4

theorem shiftRight_one (n) : n >>> 1 = n / 2 :=
  rfl

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

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

Разделы

Аффилиация

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