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]