pow_eq_one_iff_cases — Mathlib

English

For all a ∈ R and n ∈ ℕ, a^n = 1 if and only if n = 0 or a = 1 or a = −1 and n is even.

Русский

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

LaTeX

$$$$ a^n = 1 \iff n = 0 \lor a = 1 \lor \bigl(a = -1 \land \operatorname{Even}(n)\bigr). $$$$

Lean4

theorem pow_eq_one_iff_cases : a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n := by simp [← pow_eq_pow_iff_cases]

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