zero_shiftRight'

Mathlib.Data.Int.Bitwise

URI: https://scilib.ai/kg/mathlib#Int.zero_shiftRight'

English

For all integers n, 0 >>> n = 0.

Русский

Для любых n ∈ ℤ: 0 >>> n = 0.

LaTeX

$$$$ \forall n\in\mathbb{Z},\; 0 >>> n = 0. $$$$

Lean4

/-- Compare with `Int.zero_shiftRight`, which has `n : ℕ`. -/
@[simp]
theorem zero_shiftRight' (n : ℤ) : 0 >>> n = 0 :=
  zero_shiftLeft' _

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

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

Разделы

Аффилиация

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