neg_one_pow_eq_one_iff_even — Mathlib

English

In a monoid with distributive negation, if (-1) ≠ 1, then (-1)^n = 1 if and only if n is even (for all natural n).

Русский

В моноиде с распределительным отрицанием, если (-1) ≠ 1, тогда (-1)^n = 1 тогда и только тогда, когда n чётно (для всех натурных n).

LaTeX

$$$(-1)^n = 1 \\iff \\mathrm{Even}(n)$, при условии \$(-1) \\neq 1\$$$

Lean4

theorem neg_one_pow_eq_one_iff_even (h : (-1 : R) ≠ 1) : (-1 : R) ^ n = 1 ↔ Even n := by simp [neg_one_pow_eq_ite, h]

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