xor_mod_two_eq — Mathlib

English

(m ⊕ n) mod 2 = (m + n) mod 2 for all m,n.

Русский

(m ⊕ n) mod 2 = (m + n) mod 2 для всех m,n.

LaTeX

$$$ (m \oplus n) \bmod 2 = (m + n) \bmod 2 $$$

Lean4

@[simp]
theorem xor_mod_two_eq {m n : ℕ} : (m ^^^ n) % 2 = (m + n) % 2 :=
  by
  by_cases h : (m + n) % 2 = 0
  · simp only [h, mod_two_eq_zero_iff_testBit_zero, testBit_zero, xor_mod_two_eq_one, decide_not, Bool.decide_iff_dist,
      Bool.not_eq_false', beq_iff_eq, decide_eq_decide]
    cutsat
  · simp only [mod_two_ne_zero] at h
    simp only [h, xor_mod_two_eq_one]
    cutsat

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