pow_eq_neg_one_iff

Mathlib.Algebra.Order.Ring.Abs

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

English

For all a ∈ R and n ∈ ℕ, a^n = −1 iff a = −1 and n is odd.

Русский

Для любых a ∈ R и n ∈ ℕ, a^n = −1 тогда и только тогда, когда a = −1 и n нечётно.

LaTeX

$$$$ a^n = -1 \iff a = -1 \land \operatorname{Odd}(n). $$$$

Lean4

theorem pow_eq_neg_one_iff : a ^ n = -1 ↔ a = -1 ∧ Odd n := by simpa using pow_eq_neg_pow_iff (R := R) one_ne_zero

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

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

Разделы

Аффилиация

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