negOnePow_mul_self

Mathlib.Algebra.Ring.NegOnePow

URI: https://scilib.ai/kg/mathlib#Int.negOnePow_mul_self

English

For every integer n, (-1)^{n^2} = (-1)^n.

Русский

Для любого целого n выполняется (-1)^{n^2} = (-1)^n.

LaTeX

$$$$(-1)^{n^2} = (-1)^n$$$$

Lean4

@[simp]
theorem negOnePow_mul_self (n : ℤ) : (n * n).negOnePow = n.negOnePow := by
  simpa [mul_sub, negOnePow_eq_iff] using n.even_mul_pred_self

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

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

Разделы

Аффилиация

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