have z1 := hζ
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p