exact hy.eq_orderOf.symm
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
k : ℕ := lcm p q
hkpos : 0 < k
xu : Kˣ := ⋯.unit
yu : Kˣ := ⋯.unit
hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K
hxuord : orderOf ⟨xu, hxmem⟩ = p
⊢ orderOf y = q
no goals