negOnePow_eq_iff — Mathlib

English

Let n1, n2 be integers. Then (-1)^{n1} = (-1)^{n2} if and only if n1 − n2 is even.

Русский

Пусть n1, n2 — целые числа. Тогда (-1)^{n1} = (-1)^{n2} тогда и только тогда, когда разность n1 − n2 чётна.

LaTeX

$$$$(-1)^{n_1} = (-1)^{n_2} \\iff 2 \\mid (n_1 - n_2)$$$$

Lean4

theorem negOnePow_eq_iff (n₁ n₂ : ℤ) : n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂) :=
  by
  by_cases h₂ : Even n₂
  · rw [negOnePow_even _ h₂, Int.even_sub, negOnePow_eq_one_iff]
    tauto
  · rw [Int.not_even_iff_odd] at h₂
    rw [negOnePow_odd _ h₂, Int.even_sub, negOnePow_eq_neg_one_iff, ← Int.not_odd_iff_even, ← Int.not_odd_iff_even]
    tauto

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