simp
case inr.inl
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hppos : p > 0
hy : IsPrimitiveRoot y 0
⊢ (lcm p 0).totient ≤ FiniteDimensional.finrank ℚ K
no goals