lxor_bit

Mathlib.Data.Int.Bitwise

URI: https://scilib.ai/kg/mathlib#Int.lxor_bit

English

The bitwise XOR of (bit a m) and (bit b n) equals bit (a ⊕ b) (lxor m n).

Русский

Побитовый XOR: bit (a m) xor bit (b n) = bit (a ⊕ b) (lxor m n).

LaTeX

$$$$ \operatorname{lxor\_{bit}}(a,m,b,n) = \operatorname{bit}(a \oplus b)(\operatorname{lxor} m n). $$$$

Lean4

@[simp]
theorem lxor_bit (a m b n) : Int.xor (bit a m) (bit b n) = bit (xor a b) (Int.xor m n) := by
  rw [← bitwise_xor, bitwise_bit]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru