rw [Algebra.norm_algebraMap, finrank_eq_one_iff'.mpr, pow_one]
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) ((algebraMap K L) (-2)) = -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
⊢ ∃ v, v ≠ 0 ∧ ∀ (w : L), ∃ c, c • v = w