xor_bit — Mathlib

English

XOR of two bit-numbers corresponds to bit with boolean inequality and XOR of the remaining bits: bit a m ^^^ bit b n = bit (a ≠ b) (m ^^^ n).

Русский

Исключающее OR двух битовых чисел соответствует биту с логическим неравенством и XOR остальных битов: bit a m ^^^ bit b n = bit (a ≠ b) (m ^^^ n).

LaTeX

$$$$ \\mathrm{bit}\\ a\\ m \\oplus\\oplus\\ \\mathrm{bit}\\ b\\ n = \\mathrm{bit} (a \\neq b) (m \\oplus\\oplus n) $$$$

Lean4

@[simp]
theorem xor_bit : ∀ a m b n, bit a m ^^^ bit b n = bit (bne a b) (m ^^^ n) :=
  bitwise_bit

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