R : Type u_1
inst✝² : CommRing R
p n : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p ^ n + 1 = 0
R : Type u_1
inst✝² : CommRing R
p n : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p ^ n = -1
rw [eq_neg_iff_add_eq_zero]
R : Type u_1
inst✝² : CommRing R
p n : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p ^ n + 1 ^ p ^ n = 0
R : Type u_1
inst✝² : CommRing R
p n : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p ^ n + 1 = 0
nth_rw 2 [← one_pow (p ^ n)]
no goals
R : Type u_1
inst✝² : CommRing R
p n : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p ^ n + 1 ^ p ^ n = 0
rw [← add_pow_char_pow, add_left_neg, zero_pow (pow_pos (Fact.out (p := Nat.Prime p)).pos _)]