rw [← prime_isUnit_mul isUnit_one.neg, neg_mul, one_mul, neg_neg]
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
α✝ : Type ?u.198894
inst✝¹ : CommMonoidWithZero α✝
α : Type u_2
inst✝ : CommRing α
a : α
⊢ Prime (-a) ↔ Prime a
no goals