negOnePow_odd

Mathlib.Algebra.Ring.NegOnePow

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

← MathLib Explorer

English

If n is odd, then n.negOnePow = -1.

Русский

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

LaTeX

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

Lean4

theorem negOnePow_odd (n : ℤ) (hn : Odd n) : n.negOnePow = -1 :=
  by
  obtain ⟨k, rfl⟩ := hn
  simp only [negOnePow_add, negOnePow_two_mul, negOnePow_one, mul_neg, mul_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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