apply lagrange_theorem
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
t : (ZMod (p * q))ˣ
⊢ orderOf t ∣ Fintype.card (ZMod (p * q))ˣ
no goals