lnot

Mathlib.Data.Int.Bitwise

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

English

lnot flips all bits of an integer; lnot(ι(n)) = -(n+1) and lnot(-(n+1)) = ι(n).

Русский

lnot инвертирует все биты числа; lnot(ι(n)) = -(n+1) и lnot(-(n+1)) = ι(n).

LaTeX

$$$\\mathrm{lnot}(\\iota(n)) = -\\,[n+1],\\quad \\mathrm{lnot}(-\\,[n+1]) = \\iota(n)\\quad (n \\in \\mathbb{N})$$$

Lean4

/-- `lnot` flips all the bits in the binary representation of its input -/
def lnot : ℤ → ℤ
  | (m : ℕ) => -[m+1]
  | -[m+1] => m

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

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

Разделы

Аффилиация

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