negOnePow_succ

Mathlib.Algebra.Ring.NegOnePow

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

English

(n+1).negOnePow = -n.negOnePow.

Русский

(n+1).negOnePow = -n.negOnePow.

LaTeX

$$$(n + 1).negOnePow = -\, n.negOnePow$$$

Lean4

theorem negOnePow_succ (n : ℤ) : (n + 1).negOnePow = -n.negOnePow := by
  rw [negOnePow_add, negOnePow_one, mul_neg, mul_one]

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

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

Разделы

Аффилиация

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