zpow_eq_neg_one_iff₀ — Mathlib

English

Let α be a linearly ordered field with IsStrictOrderedRing. For any a ∈ α and n ∈ ℤ, a^n = -1 iff a = -1 and Odd n.

Русский

Пусть α — упорядоченное поле с IsStrictOrderedRing. Для любого a ∈ α и n ∈ ℤ, a^n = -1 тогда и только если a = -1 и n нечётно.

LaTeX

$$$\forall a \in \alpha, \forall n \in \mathbb{Z}, a^{n} = -1 \iff (a = -1) \land \mathrm{Odd}(n)$$$

Lean4

theorem zpow_eq_neg_one_iff₀ : a ^ n = -1 ↔ a = -1 ∧ Odd n := by simpa using zpow_eq_neg_zpow_iff₀ (α := α) one_ne_zero

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