even_xor — Mathlib

English

Let m,n be natural numbers. The bitwise exclusive OR of m and n is even if and only if m and n have the same parity (both even or both odd).

Русский

Пусть m,n ∈ ℕ. Побитовая операция XOR между m и n порождает чётное число тогда и только тогда, когда m и n имеют одинаковую чётность (обе чётные или обе нечётные).

LaTeX

$$$ \operatorname{Even}(m \oplus n) \iff (\operatorname{Even}(m) \iff \operatorname{Even}(n))$$$

Lean4

@[simp]
theorem even_xor {m n : ℕ} : Even (m ^^^ n) ↔ (Even m ↔ Even n) :=
  by
  simp only [even_iff, xor_mod_two_eq]
  cutsat

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