bitwise_xor — Mathlib

English

The bitwise XOR operation coincides with the integer XOR: bitwise xor = Int.xor.

Русский

Побитовая операция XOR совпадает с целочисленным XOR: bitwise xor = Int.xor.

LaTeX

$$$$ \operatorname{bitwise} \text{ xor } = \operatorname{Int}.xor. $$$$

Lean4

theorem bitwise_xor : bitwise xor = Int.xor := by
  funext m n
  rcases m with m | m <;> rcases n with n | n <;>
        try { rfl
        } <;>
      simp only [bitwise, natBitwise, Bool.not_false, Bool.bne_eq_xor, cond_false, cond_true, negSucc.injEq,
        Bool.false_xor, Bool.true_xor, Bool.not_true, Int.xor, HXor.hXor, XorOp.xor, Nat.xor] <;>
    simp

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