ldiff_bit — Mathlib

English

The bitwise difference with and with not yields bit with and-not parity: ldiff (bit a m) (bit b n) = bit (a ∧ ¬b) (ldiff m n).

Русский

Побитовая разность через и с не равно bit (a ∧ ¬b) (ldiff m n).

LaTeX

$$$$ \operatorname{ldiff\_{bit}}(a,m,b,n) = \operatorname{bit}(a \land \lnot b)(\operatorname{ldiff} m n). $$$$

Lean4

@[simp]
theorem ldiff_bit (a m b n) : ldiff (bit a m) (bit b n) = bit (a && not b) (ldiff m n) := by
  rw [← bitwise_diff, bitwise_bit]

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