def Hex.Nat.orderOf (a n : Nat) : Nat

Multiplicative order of a modulo n: the least k > 0 with a ^ k % n = 1 % n when 1 < n and Nat.Coprime a n, and 0 on every other input.

Equations

• Hex.Nat.orderOf a n = if 1 < n ∧ a.Coprime n then Hex.Nat.orderOfAux✝ (a % n) n n 1 (a % n) else 0

theorem Hex.Nat.coprime_of_pow_mod_eq_one {a n k : Nat} (h1 : 1 < n) (hk : 0 < k) (h : a ^ k % n = 1 % n) : a.Coprime n

A power congruent to 1 forces coprimality of the base: the gcd divides both a ^ k and n, hence their remainder 1.

theorem Hex.Nat.pow_pred_mod {p a : Nat} (hp : Prime p) (h : a.Coprime p) : a ^ (p - 1) % p = 1 % p

Fermat's little theorem in multiplicative form, from the residue form pow_prime_mod by cancelling one factor of a.

theorem Hex.Nat.one_lt_of_orderOf_pos {a n : Nat} (h : 0 < orderOf a n) : 1 < n

A positive order certifies a nontrivial modulus.

theorem Hex.Nat.coprime_of_orderOf_pos {a n : Nat} (h : 0 < orderOf a n) : a.Coprime n

A positive order certifies coprimality.

theorem Hex.Nat.orderOf_pow_mod {a n : Nat} (h : 0 < orderOf a n) : a ^ orderOf a n % n = 1 % n

A positive order is an exponent sending a to 1 modulo n.

theorem Hex.Nat.orderOf_min {a n : Nat} (h : 0 < orderOf a n) (j : Nat) : 0 < j → j < orderOf a n → a ^ j % n ≠ 1 % n

Minimality of a positive order among positive exponents.

theorem Hex.Nat.orderOf_pos_of_pow_eq_one {a n k : Nat} (h1 : 1 < n) (hk : 0 < k) (h : a ^ k % n = 1 % n) : 0 < orderOf a n

A witness exponent produces a positive order: the scan up to the witness finds the least one, pigeonhole bounds it by n, and the definitional scan up to n therefore also finds it.

theorem Hex.Nat.orderOf_dvd_of_pow_eq_one {a n k : Nat} (h1 : 1 < n) (hk : 0 < k) (h : a ^ k % n = 1 % n) : orderOf a n ∣ k

The order divides every exponent sending a to 1 modulo n.

theorem Hex.Nat.pow_eq_one_of_orderOf_dvd {a n k : Nat} (h : 0 < orderOf a n) (hd : orderOf a n ∣ k) : a ^ k % n = 1 % n

Any multiple of a positive order sends a to 1 modulo n.

theorem Hex.Nat.orderOf_dvd_pred {p a : Nat} (hp : Prime p) (h : a.Coprime p) : orderOf a p ∣ p - 1

The order of a unit modulo a prime divides p - 1.

theorem Hex.Nat.prime_pow_dvd_orderOf {q j m a p : Nat} (hq : Prime q) (hj : q ^ j ∣ m) (h1 : 1 < p) (hm : a ^ m % p = 1 % p) (hne : a ^ (m / q) % p ≠ 1 % p) : q ^ j ∣ orderOf a p

Prime-power extraction into the order: if q ^ j ∣ m, a ^ m ≡ 1, and a ^ (m / q) ≢ 1 modulo p, then q ^ j divides the order of a. Stated with q ^ j ∣ m as a hypothesis so no valuation API is needed.

theorem Hex.Nat.sq_roots_of_one {p x : Nat} (hp : Prime p) (hx : x < p) (h : x * x % p = 1 % p) : x = 1 ∨ x = p - 1

Modulo a prime, the square roots of 1 are 1 and p - 1: the factorisation x² - 1 = (x - 1)(x + 1) and Euclid's lemma.

theorem Hex.Nat.orderOf_pos {a n : Nat} (h1 : 1 < n) (h : a.Coprime n) : 0 < orderOf a n

Every coprime base has a positive order: pigeonhole among the n + 1 residues a ^ 0 % n, …, a ^ n % n finds a repeat, and cancellation turns the repeat into a witness exponent.