n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a ↑(ZMod.val i)) = 2 * n / Nat.gcd (2 * n) (ZMod.val i)
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a i) = 2 * n / Nat.gcd (2 * n) (ZMod.val i)
conv_lhs => rw [← ZMod.nat_cast_zmod_val i]
no goals
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a ↑(ZMod.val i)) = 2 * n / Nat.gcd (2 * n) (ZMod.val i)
rw [← a_one_pow, orderOf_pow, orderOf_a_one]