neg_one_pow

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Even.neg_one_pow

English

If n is even, then (-1)^n = 1 in any Monoid with distributive negation.

Русский

Если n чётно, то (-1)^n = 1 в любом моноиде с распределительным отрицанием.

LaTeX

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

Lean4

theorem neg_one_pow (h : Even n) : (-1 : α) ^ n = 1 := by rw [h.neg_pow, one_pow]

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

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

Разделы

Аффилиация

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