negOnePow_eq_neg_one_iff

Mathlib.Algebra.Ring.NegOnePow

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

← MathLib Explorer

English

NegOnePow(n) = -1 iff n is odd.

Русский

NegOnePow(n) = -1 тогда и только тогда, когда n нечётно.

LaTeX

$$$n.negOnePow = -1 \iff Odd(n)$$$

Lean4

theorem negOnePow_eq_neg_one_iff (n : ℤ) : n.negOnePow = -1 ↔ Odd n :=
  by
  constructor
  · intro h
    rw [← Int.not_even_iff_odd]
    intro h'
    rw [negOnePow_even _ h'] at h
    contradiction
  · exact negOnePow_odd n

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

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

Разделы

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

Аффилиация

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