Integer_to_Power_of_Multiple_of_Order

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

modular-arithmeticnumber-theoryproofwiki

Let a and n be coprime integers. Let c be the multiplicative order of a modulo n. Then a^k = 1 mod n iff c divides k.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Nat.GCD.Basic

Formal statement

theorem Integer_to_Power_of_Multiple_of_Order (a n c k : ℕ) (hn : 0 < n) (hcop : Nat.Coprime a n) (hc : 0 < c) (hord : a ^ c ≡ 1 [MOD n]) (hk : c ∣ k) : a ^ k ≡ 1 [MOD n] := by sorry

Source

https://proofwiki.org/wiki/Integer_to_Power_of_Multiple_of_Order

View graph