testBit_lxor — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem testBit_lxor (m n k) : testBit (Int.xor m n) k = xor (testBit m k) (testBit n k) := by
  rw [← bitwise_xor, testBit_bitwise]

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