Integer_has_Multiplicative_Order_Modulo_n_iff_Coprime_to_n
Provedcoprime-integersmodular-arithmeticproofwiki
Let a and n be integers. If the multiplicative order of a modulo n exists, then a and n are coprime.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.GCD.Basic
Formal statement
theorem Integer_has_Multiplicative_Order_Modulo_n_iff_Coprime_to_n (a n : ℕ) (hn : 0 < n) (h : ∃ k : ℕ, 0 < k ∧ a ^ k ≡ 1 [MOD n]) : Nat.Coprime a n := by sorry
Source