neg_one_zpow

Mathlib.Algebra.Field.Power

URI: https://scilib.ai/kg/mathlib#Odd.neg_one_zpow

English

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

Русский

Если n нечётно, то (-1)^n = -1.

LaTeX

$$$\text{Odd}(n) \Rightarrow (-1)^n = -1$$$

Lean4

theorem neg_one_zpow (h : Odd n) : (-1 : α) ^ n = -1 := by rw [h.neg_zpow, one_zpow]

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

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

Разделы

Аффилиация

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