neg_one_pow_congr

Mathlib.Algebra.Ring.Parity

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

English

If m,n have the same parity, then (-1)^m = (-1)^n.

Русский

Если m и n имеют одну и ту же парность, то (-1)^m = (-1)^n.

LaTeX

$$$\forall m,n,\n Iff(\mathrm{Even}(m), \mathrm{Even}(n)) \Rightarrow (-1)^m = (-1)^n.$$$

Lean4

theorem neg_one_pow_congr (h : Even m ↔ Even n) : (-1 : R) ^ m = (-1) ^ n := by simp [h, neg_one_pow_eq_ite]

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

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

Разделы

Аффилиация

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