zpow_eq_one_iff_of_ne_zero₀ — Mathlib

English

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

Русский

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

LaTeX

$$$\forall a \in \alpha, \forall n \in \mathbb{Z}, n \ne 0 \Rightarrow a^{n} = 1 \iff (a = 1) \lor (a = -1 \land \mathrm{Even}(n))$$$

Lean4

theorem zpow_eq_one_iff_of_ne_zero₀ (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n := by
  simp [← zpow_eq_zpow_iff_of_ne_zero₀ hn]

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