neg_one_pow_succAbove_add_predAbove

English

The sign (-1) raised to the parities given by succAbove/predAbove relations relates to the negated power of the sum i+j.

Русский

Знак $(-1)$ в степени, заданной отношениями succAbove/predAbove, равен минусу степени $(-1)$ от суммы $i+j$.

LaTeX

$$$-1^{\,i.succAbove j + j.predAbove i} = -\,(-1)^{i+j}.$$$

Lean4

theorem neg_one_pow_succAbove_add_predAbove {R : Type*} [Monoid R] [HasDistribNeg R] (i : Fin (n + 1)) (j : Fin n) :
    (-1 : R) ^ (i.succAbove j + j.predAbove i : ℕ) = -(-1) ^ (i + j : ℕ) :=
  by
  rw [← neg_one_mul (_ ^ _), ← pow_succ', neg_one_pow_congr]
  rw [even_succAbove_add_predAbove, Nat.even_add_one, Nat.not_even_iff_odd]

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