Orders of residues

Let ℓ be a prime and a > 1 a natural number. The multiplicative order of a modulo ℓ ^ r has unbounded ℓ-adic valuation as r grows: for every j, the power ℓ ^ j divides it for all large r (ZMod.eventually_pow_dvd_orderOf_natCast).

When ℓ ∣ a the residue of a is not a unit and its order is 0 from r = 1 on. Otherwise the order divides φ(ℓ ^ r) = ℓ ^ (r - 1) (ℓ - 1), so if ℓ ^ j did not divide it, it would divide the number ℓ ^ (j - 1) (ℓ - 1), which does not depend on r; then ℓ ^ r would divide the positive number a ^ (ℓ ^ (j - 1) (ℓ - 1)) - 1 for every r, which is absurd.

For the residue a = 𝔑𝔭 of a prime 𝔭 ∤ ℓ of a number field, this order is the residue degree of 𝔭 in the cyclotomic extension of level ℓ ^ r, so the statement says that these residue degrees become divisible by any given power of ℓ along the cyclotomic tower.

A residue whose order is φ(n) is a primitive root modulo n. A primitive root modulo n is one modulo every divisor of n, and for an odd prime p a primitive root modulo p ² is one modulo every power of p.

The order of q modulo n decides which of the numbers q ^ k - 1 are divisible by n: those with k a multiple of the order. Modulo a prime p, an element of even order 2 * m has m-th power -1, so if a / b has order 2 * m then p divides a ^ k + b ^ k exactly for the odd multiples k of m; for b = 1 this decides which q ^ k + 1 are divisible by p.

Main results

• ZMod.orderOf_natCast_dvd_orderOf_natCast: for m ∣ n, the order of a modulo m divides its order modulo n.
• ZMod.eventually_pow_dvd_orderOf_natCast: for every j, ℓ ^ j divides the order of a modulo ℓ ^ r for all large r.
• ZMod.isUnit_of_orderOf_eq_totient, ZMod.zpowers_eq_top_of_orderOf_eq_totient: a residue of order φ(n) is a unit, and generates (ℤ/n)ˣ.
• ZMod.exists_orderOf_natCast_eq_totient: if (ℤ/n)ˣ is cyclic, some natural number is a primitive root modulo n.
• ZMod.orderOf_natCast_eq_totient_of_dvd: a primitive root modulo n is a primitive root modulo every divisor of n.
• ZMod.orderOf_natCast_prime_pow_eq_totient: for odd p, a primitive root modulo p ² is a primitive root modulo every p ^ e.
• ZMod.dvd_pow_sub_one_iff_orderOf_natCast_dvd: for q > 0, n ∣ q ^ k - 1 iff the order of q modulo n divides k.
• Nat.Prime.dvd_pow_add_pow_iff_of_orderOf_eq_two_mul: if a / b has order 2 * m ≠ 0 modulo a prime p, then p ∣ a ^ k + b ^ k iff m ∣ k and ¬ 2 * m ∣ k.
• Nat.Prime.dvd_pow_add_one_iff_of_orderOf_natCast_eq_two_mul: if q has order 2 * m ≠ 0 modulo a prime p, then p ∣ q ^ k + 1 iff m ∣ k and ¬ 2 * m ∣ k.

References

• K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, Chapter 4, §1, Theorem 2.

theorem ZMod.orderOf_natCast_dvd_orderOf_natCast {m n : ℕ} (h : m ∣ n) (a : ℕ) : orderOf ↑a ∣ orderOf ↑a

For m ∣ n, the order of a natural number a modulo m divides its order modulo n, since reduction modulo m is a ring homomorphism ZMod n →+* ZMod m.

theorem ZMod.eventually_pow_dvd_orderOf_natCast {ℓ : ℕ} (hℓ : Nat.Prime ℓ) {a : ℕ} (ha : 1 < a) (j : ℕ) : ∀ᶠ (r : ℕ) in Filter.atTop, ℓ ^ j ∣ orderOf ↑a

For a prime ℓ and a natural number a > 1, every power ℓ ^ j divides the multiplicative order of a modulo ℓ ^ r for all large r.

Primitive roots

theorem ZMod.isUnit_of_orderOf_eq_totient {n : ℕ} [NeZero n] {x : ZMod n} (h : orderOf x = n.totient) : IsUnit x

A residue modulo n whose order is φ(n) is a unit.

theorem ZMod.zpowers_eq_top_of_orderOf_eq_totient {n : ℕ} [NeZero n] {u : (ZMod n)ˣ} (h : orderOf u = n.totient) : Subgroup.zpowers u = ⊤

A unit modulo n whose order is φ(n) generates (ℤ/n)ˣ.

theorem ZMod.exists_orderOf_natCast_eq_totient {n : ℕ} [NeZero n] [IsCyclic (ZMod n)ˣ] : ∃ (g : ℕ), orderOf ↑g = n.totient

If (ℤ/n)ˣ is cyclic, some natural number is a primitive root modulo n.

theorem ZMod.orderOf_natCast_eq_totient_of_dvd {d n g : ℕ} [NeZero n] (hdn : d ∣ n) (hg : orderOf ↑g = n.totient) : orderOf ↑g = d.totient

A primitive root modulo n is a primitive root modulo every divisor d of n.

theorem ZMod.orderOf_natCast_prime_pow_eq_totient {p g : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) (hg : orderOf ↑g = (p ^ 2).totient) (e : ℕ) : orderOf ↑g = (p ^ e).totient

A primitive root modulo p ² is a primitive root modulo every power of p, for an odd prime p.

Divisibility of q ^ k - 1 and q ^ k + 1

theorem ZMod.dvd_pow_sub_one_iff_orderOf_natCast_dvd {n q : ℕ} (hq : 0 < q) (k : ℕ) : n ∣ q ^ k - 1 ↔ orderOf ↑q ∣ k

For a positive natural number q and any modulus n, n divides q ^ k - 1 if and only if the order of q modulo n divides k.

theorem Nat.Prime.dvd_pow_add_pow_iff_of_orderOf_eq_two_mul {p a b m : ℕ} (hp : Prime p) (h : orderOf (↑a * (↑b)⁻¹) = 2 * m) (hm : m ≠ 0) (k : ℕ) : p ∣ a ^ k + b ^ k ↔ m ∣ k ∧ ¬2 * m ∣ k

Suppose that a / b has order 2 * m modulo a prime p, with m ≠ 0. Then p divides a ^ k + b ^ k exactly for the odd multiples k of m. The inverse is that of ZMod p, which is the field inverse since p is prime; the hypothesis on the order forces p ∤ b.

theorem Nat.Prime.dvd_pow_add_one_iff_of_orderOf_natCast_eq_two_mul {p q m : ℕ} (hp : Prime p) (h : orderOf ↑q = 2 * m) (hm : m ≠ 0) (k : ℕ) : p ∣ q ^ k + 1 ↔ m ∣ k ∧ ¬2 * m ∣ k

If q has order 2 * m modulo a prime p, with m ≠ 0, then p divides q ^ k + 1 exactly for the odd multiples k of m.