exact hζ.zeta_sub_one_prime'
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ Prime (↑hζ.unit' - 1)
no goals