simpa only [Algebra.algebraMap_eq_smul_one] using surjective_of_isCyclotomicExtension_two K L w
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
w : L
⊢ ∃ c, c • 1 = w
no goals