have h := prim_coe η (nth_roots_prim hη hne1)
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
⊢ _root_.Prime (1 - η)
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h : IsPrimitiveRoot ↑η ↑p
⊢ _root_.Prime (1 - η)