Theorem: prime_neg_iff (FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean)

State before:
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
Tactic:
rw [← prime_isUnit_mul isUnit_one.neg, neg_mul, one_mul, neg_neg]
State after:
no goals