neg_one_pow_eq_neg_one_iff_odd

Mathlib.Algebra.Ring.Parity

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

English

If (-1) ≠ 1, then (-1)^n = -1 iff n is odd.

Русский

Если (-1) ≠ 1, тогда (-1)^n = -1 тогда и только тогда, когда n нечётно.

LaTeX

$$$(-1)^n = -1 \iff \mathrm{Odd}(n).$$$

Lean4

theorem neg_one_pow_eq_neg_one_iff_odd (h : (-1 : R) ≠ 1) : (-1 : R) ^ n = -1 ↔ Odd n := by
  simp [neg_one_pow_eq_ite, h.symm]

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

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

Разделы

Аффилиация

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