n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r ↑(ZMod.val i)) = n / Nat.gcd n (ZMod.val i)
n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r i) = n / Nat.gcd n (ZMod.val i)
conv_lhs => rw [← ZMod.nat_cast_zmod_val i]
no goals
n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r ↑(ZMod.val i)) = n / Nat.gcd n (ZMod.val i)
rw [← r_one_pow, orderOf_pow, orderOf_r_one]