shiftRight_negSucc

Mathlib.Data.Int.Bitwise

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

English

For natural m and n, the right shift of the negation successor −(m+1) by n equals the negation of m shifted right by n+1.

Русский

Для натуральных m,n: -[m+1] >>> n = -[m >>> (n+1)].

LaTeX

$$$$ \forall m,n\in\mathbb{N},\; -[m+1] \\>\\>\\> (n) = -[m \/>>> (n+1)]. $$$$

Lean4

@[simp]
theorem shiftRight_negSucc (m n : ℕ) : -[m+1] >>> (n : ℤ) = -[m >>> n+1] := by cases n <;> rfl

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

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

Разделы

Аффилиация

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