bodd_subNatNat — Mathlib

English

For naturals m,n, parity of subNatNat(m,n) equals xor of parities: bodd(subNatNat m n) = m.bodd ⊕ n.bodd.

Русский

Для натуральных m,n паритет subNatNat(m,n) равен XOR паритетов m и n.

LaTeX

$$$\\mathrm{bodd}(\\mathrm{subNatNat}(m,n)) = \\mathrm{xor}(m.\\mathrm{bodd}, n.\\mathrm{bodd})$$$

Lean4

@[simp]
theorem bodd_subNatNat (m n : ℕ) : bodd (subNatNat m n) = xor m.bodd n.bodd := by
  apply subNatNat_elim m n fun m n i => bodd i = xor m.bodd n.bodd <;> intro i j <;>
        simp only [Int.bodd, Nat.bodd_add] <;>
      cases Nat.bodd i <;>
    simp

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