bodd_add — Mathlib

English

For all m,n ∈ ℤ, bodd(m+n) equals the exclusive or of bodd(m) and bodd(n): bodd(m+n) = bodd(m) ⊕ bodd(n).

Русский

Для любых m,n ∈ ℤ справедливо: bodd(m+n) = bodd(m) ⊕ bodd(n).

LaTeX

$$$$ \forall m,n \in \mathbb{Z},\ \operatorname{bodd}(m+n) = \operatorname{bodd}(m) \oplus \operatorname{bodd}(n). $$$$

Lean4

@[simp]
theorem bodd_add (m n : ℤ) : bodd (m + n) = xor (bodd m) (bodd n) := by
  rcases m with m | m <;> rcases n with n | n <;>
      simp only [ofNat_eq_coe, ofNat_add_negSucc, negSucc_add_ofNat, negSucc_add_negSucc, bodd_subNatNat,
        ← Nat.cast_add] <;>
    simp [bodd, Bool.xor_comm]

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