shiftLeft_negSucc

Mathlib.Data.Int.Bitwise

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

English

For natural m and n, the left shift of the negation successor −(m+1) by n equals the negation of Nat.shiftLeft' true m n+1.

Русский

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

LaTeX

$$$$ \forall m,n\in\mathbb{N},\; -[m+1] \ \mathrm{<<<}\ n = -[\mathrm{Nat.shiftLeft'}\ true\ m\ (n+1)]. $$$$

Lean4

@[simp]
theorem shiftLeft_negSucc (m n : ℕ) : -[m+1] <<< (n : ℤ) = -[Nat.shiftLeft' true m n+1] :=
  rfl

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

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

Разделы

Аффилиация

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