Theorem: neg_one_eq_one_iff_two_eq_zero (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
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
Tactic:
rw [neg_eq_iff_add_eq_zero, one_add_one_eq_two]
State after:
no goals