neg_one_pow_expChar_pow — Mathlib

English

Let R be a ring and p a prime with ExpChar R p. Then\n (-1)^p^n = -1.

Русский

Пусть R — кольцо, p — простое, ExpChar R p. Тогда\n (-1)^{p^n} = -1.

LaTeX

$$$(-1)^{p^n} = -1$$$

Lean4

theorem neg_one_pow_expChar_pow : (-1 : R) ^ p ^ n = -1 :=
  by
  rw [eq_neg_iff_add_eq_zero]
  nth_rw 2 [← one_pow (p ^ n)]
  rw [← add_pow_expChar_pow_of_commute _ _ (Commute.one_right _), neg_add_cancel,
    zero_pow (pow_ne_zero _ <| expChar_ne_zero R p)]

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