ldiff — Mathlib

English

ldiff performs bitwise set difference: a ∧ ¬b on each bit.

Русский

ldiff выполняет побитовое различие: a ∧ ¬b по каждому биту.

LaTeX

$$$\\mathrm{ldiff}: \\mathbb{Z} \\to \\mathbb{Z} \\to \\mathbb{Z}$$$

Lean4

/-- `ldiff a b` performs bitwise set difference. For each corresponding
  pair of bits taken as Booleans, say `aᵢ` and `bᵢ`, it applies the
  Boolean operation `aᵢ ∧ ¬bᵢ` to obtain the `iᵗʰ` bit of the result. -/
def ldiff : ℤ → ℤ → ℤ
  | (m : ℕ), (n : ℕ) => Nat.ldiff m n
  | (m : ℕ), -[n+1] => m &&& n
  | -[m+1], (n : ℕ) => -[m ||| n+1]
  | -[m+1], -[n+1] => Nat.ldiff n m

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