apply isRoot_of_unity_of_root_cyclotomic _ hhl
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
⊢ ⟨x, hx⟩ ^ l = 1
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
⊢ l ∈ l.divisors