pow_eq_one_iff_of_ne_zero — Mathlib

English

Let R be a ring with a linear order and n a natural number with n ≠ 0. Then a^n = 1 if and only if a = 1 or a = −1 and n is even.

Русский

Пусть R — кольцо, упорядоченное галуа, и n ∈ ℕ с n ≠ 0. Тогда a^n = 1 тогда и только тогда, когда a = 1 или a = −1 и n чётно.

LaTeX

$$$$ \forall a \in R, \forall n \in \mathbb{N},\ n \neq 0 \Rightarrow a^n = 1 \iff a = 1 \lor \bigl(a = -1 \land \operatorname{Even}(n)\bigr). $$$$

Lean4

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

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