neg_one_pow_eq_ite — Mathlib

English

For a ring R with appropriate negation, (-1)^n equals 1 if n is even, and -1 if n is odd.

Русский

Для кольца R с подходящим определением отрицания, (-1)^n равняется 1, если n чётно, и −1, если n нечётно.

LaTeX

$$$(-1)^n = \begin{cases} 1, & \text{if } \mathrm{Even}(n), \\ -1, & \text{otherwise}. \end{cases}$$$

Lean4

theorem neg_one_pow_eq_ite : (-1 : R) ^ n = if Even n then 1 else (-1) := by
  cases even_or_odd n with
  | inl h => rw [h.neg_one_pow, if_pos h]
  | inr h => rw [h.neg_one_pow, if_neg (by simpa using h)]

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