zpow_eq_one_iff_cases₀ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem zpow_eq_one_iff_cases₀ : a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n := by simp [← zpow_eq_zpow_iff_cases₀]

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