rw [neg_eq_iff_add_eq_zero, one_add_one_eq_two]
p : ℕ+
K : Type ?u.162504
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
M : Type u_1
inst✝ : AddGroupWithOne M
⊢ -1 = 1 ↔ 2 = 0
no goals