neg_one_pow_eq_or — Mathlib

English

For any a in a ring with distributive negation, and any n ∈ N, (-a)^n = (-1)^n · a^n.

Русский

Для любого a в кольце с распределимым отрицанием и любого n ∈ ℕ выполняется (-a)^n = (-1)^n · a^n.

LaTeX

$$$ (-a)^n = (-1)^n \\cdot a^n $$$

Lean4

theorem neg_one_pow_eq_or : ∀ n : ℕ, (-1 : R) ^ n = 1 ∨ (-1 : R) ^ n = -1
  | 0 => Or.inl (pow_zero _)
  | n + 1 =>
    (neg_one_pow_eq_or n).symm.imp (fun h ↦ by rw [pow_succ, h, neg_one_mul, neg_neg])
      (fun h ↦ by rw [pow_succ, h, one_mul])

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