rw [nthRoots_one_eq_biUnion_primitiveRoots' hζ'] at hη
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 ↑⋯.unit' ↑p
⊢ IsPrimitiveRoot η ↑p
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ (↑p).divisors.biUnion fun i => primitiveRoots i (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
⊢ IsPrimitiveRoot η ↑p