English
For a ∈ ℕ and n ∈ ℕ with gcd(n,a) defined, the order of a in ZMod n is n / gcd(n,a).
Русский
Для a ∈ ℕ и n ∈ ℕ порядок a в ZMod n равен n / gcd(n,a).
LaTeX
$$$ \operatorname{addOrderOf}(a : \mathrm{ZMod}\, n) = \dfrac{n}{\gcd(n,a)} $$$
Lean4
/-- This lemma works in the case in which `ZMod n` is not infinite, i.e. `n ≠ 0`. The version
where `a ≠ 0` is `addOrderOf_coe'`. -/
@[simp]
theorem addOrderOf_coe (a : ℕ) {n : ℕ} (n0 : n ≠ 0) : addOrderOf (a : ZMod n) = n / n.gcd a :=
by
rcases a with - | a
· simp only [Nat.cast_zero, addOrderOf_zero, Nat.gcd_zero_right, Nat.pos_of_ne_zero n0, Nat.div_self]
rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a.succ_ne_zero, ZMod.addOrderOf_one]
