§5, p. 1498 — the order of x mod n is the lcm of its orders mod the prime powers p_i^{α_i}

Let $n = \prod_{i=1}^k p_i^{\alpha_i}$ be the prime factorization of $n \ge 1$, let $x$ be a unit modulo $n$ with order $r$, and let $r_i$ be the order of $x \bmod p_i^{\alpha_i}$. Then

This reduces questions about the order modulo $n$ to the orders modulo the prime powers, where the unit groups are cyclic when $p_i$ is odd.

Formalization Note The $r_i$ are localOrder n u p for p ∈ n.primeFactors, and the lcm is Finset.lcm over n.primeFactors (equal to $1$ when $n = 1$). The hypothesis $0 < n$ replaces Shor's standing "$n$ odd"; oddness is not needed here, while $n = 0$ must be excluded because ZMod 0 is $\mathbb{Z}$.