shiftLeft_sub

Mathlib.Data.Int.Bitwise

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

English

For all integers m, natural n and integer k, m <<< (n − k) equals (m <<< (n)) >>> k.

Русский

Для любых m ∈ ℤ, n ∈ ℕ, k ∈ ℤ: m <<< (n − k) = (m <<< n) >>> k.

LaTeX

$$$$ \forall m\in\mathbb{Z},\; \forall n\in\mathbb{N},\; \forall k\in\mathbb{Z},\; m <<< (n-k) = (m <<< (n)) >>> k. $$$$

Lean4

theorem shiftLeft_sub (m : ℤ) (n : ℕ) (k : ℤ) : m <<< (n - k) = (m <<< (n : ℤ)) >>> k :=
  shiftLeft_add' _ _ _

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

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

Разделы

Аффилиация

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