testBit_ldiff — Mathlib

English

For all integers m, n and natural k, testBit (ldiff m n) k equals (testBit m k) and not (testBit n k).

Русский

Для любых целых m, n и натурального k: k-й бит результата ldiff m n равен конъюнкции k-го бита m и отрицания k-го бита n.

LaTeX

$$$$\forall m,n\in\mathbb{Z},\; \forall k\in\mathbb{N},\; \mathrm{testBit}(\mathrm{ldiff}\, m\, n)\ k = (\mathrm{testBit}\, m\ k)\land\lnot(\mathrm{testBit}\, n\ k).$$$$

Lean4

@[simp]
theorem testBit_ldiff (m n k) : testBit (ldiff m n) k = (testBit m k && not (testBit n k)) := by
  rw [← bitwise_diff, testBit_bitwise]

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