ofAdd_neg_one_pow_comm — Mathlib

English

For all integers a and natural n, ((−1)^{−a})^{n} = (−1)^{a n}.

Русский

Для всех целых a и натуральных n выполняется ((−1)^{−a})^{n} = (−1)^{a n}.

LaTeX

$$$\\\\forall a \\\\in \\\\mathbb{Z}, \\\\forall n \\\\in \\\\mathbb{N}, ((-1)^{-a})^{n} = (-1)^{a n}$$$

Lean4

@[deprecated exp_neg (since := "2025-05-17")]
theorem ofAdd_neg_one_pow_comm (a : ℤ) (n : ℕ) : ((↑(ofAdd (-1 : ℤ)) : ℤᵐ⁰) ^ (-a)) ^ n = ofAdd (n : ℤ) ^ a :=
  show (exp (-1 : ℤ) ^ (-a)) ^ n = exp (n : ℤ) ^ a by simp [mul_comm]

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