have : (algebraMap R K) (hζ.unit' : R) = ζ := rfl
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ζ ↑p
this : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p