even_xor'_odd' — Mathlib

English

For integers m and n, m+n is even if and only if m and n have the same parity (both even or both odd).

Русский

Для целых m и n сумма m+n чётна тогда и только тогда, когда m и n имеют одинаковую парность (оба чётные или оба нечётные).

LaTeX

$$$\\operatorname{Even}(m+n) \\iff (\\operatorname{Odd}(m) \\iff \\operatorname{Odd}(n))$$$

Lean4

theorem even_xor'_odd' (n : ℤ) : ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1) := by
  rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩) <;>
    · use k
      simp only [Xor'] -- Perhaps `grind` needs a normalization rule for `Xor'`?

      grind

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