rw [hζ.eq_neg_one_of_two_right]
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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) (ζ - 1) = -2
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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) (-1 - 1) = -2