bodd_neg — Mathlib

English

For every integer n, the parity of -n equals the parity of n; parity is invariant under sign change: bodd(-n) = bodd(n).

Русский

Для каждого целого числа n парность числа -n равна парности n; парность сохраняется при смене знака: bodd(-n) = bodd(n).

LaTeX

$$$ ∀ n ∈ \mathbb{Z},\ bodd(-n) = bodd(n). $$$

Lean4

@[simp]
theorem bodd_neg (n : ℤ) : bodd (-n) = bodd n := by
  cases n <;> simp only [← negOfNat_eq, bodd_negOfNat, neg_negSucc] <;> simp [bodd]

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