neg_one_pow_eq_pow_mod_two

Mathlib.Algebra.Ring.Commute

URI: https://scilib.ai/kg/mathlib#neg_one_pow_eq_pow_mod_two

English

For every n ∈ ℕ, (-1)^n equals (-1)^(n mod 2).

Русский

Для каждого n ∈ ℕ выполняется, что (-1)^n = (-1)^(n mod 2).

LaTeX

$$$ (-1)^n = (-1)^{\, n \\bmod 2} $$$

Lean4

theorem neg_one_pow_eq_pow_mod_two (n : ℕ) : (-1 : R) ^ n = (-1) ^ (n % 2) := by
  rw [← Nat.mod_add_div n 2, pow_add, pow_mul]; simp [sq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru