Regular integers modulo n

TheoremMorgado's formula as a sum over unitary divisors#✓fully proved

For every positive integer \(n\), the number of residue classes \(m \in \mathbb{Z}/n\mathbb{Z}\) for which the equation \(m^2 x = m\) has a solution \(x \in \mathbb{Z}/n\mathbb{Z}\) equals the sum of \(\varphi(d)\) over the unitary divisors \(d\) of \(n\) (the positive divisors \(d\) of \(n\) with \(\gcd(d, n/d) = 1\)), where \(\varphi\) is Euler's totient function.

theorem ncard_regular_eq_sum_totient_unitaryDivisors (n : ℕ) (hn : 0 < n) :
    Set.ncard {m : ZMod n | ∃ x : ZMod n, m ^ 2 * x = m} =
      ∑ d ∈ n.unitaryDivisors, Nat.totient d
Uses 1 · Used by 1
Statement usesUnitary divisors
Used byMorgado's formula for the number of regular residues

TheoremMorgado's formula for the number of regular residues#✓fully proved

Let \(n\) be a positive integer. Call a residue class \(m \in \mathbb{Z}/n\mathbb{Z}\) regular if the equation \(m^2 x = m\) has a solution \(x \in \mathbb{Z}/n\mathbb{Z}\), and let \(\varrho(n)\) be the number of regular residue classes. Let \(U(n)\) be the set of positive divisors \(d\) of \(n\) with \(\gcd(d, n/d) = 1\). Then

\[\varrho(n) = \sum_{d \in U(n)} \varphi(d),\]

where \(\varphi\) is Euler's totient function.

The sequence \(\varrho(1), \varrho(2), \ldots\) is OEIS A055653.

theorem morgado_card_regular_modulo (n : ℕ) (hn : 0 < n) :
    Set.ncard {m : ZMod n | ∃ x : ZMod n, m ^ 2 * x = m} =
      ∑ d ∈ n.divisors.filter (fun d => Nat.Coprime d (n / d)), Nat.totient d
Sources
  • Klaus Dohmen and Mandy Lange-Geisler, "On the Number of Regular Integers Modulo n and Its Significance for Cryptography", Journal of Integer Sequences 29 (2026), Article 26.2.4, Definition [Morgado 1972] lines 108-112 and Theorem [Morgado 1972] (equation eq:2) lines 127-132: https://cs.uwaterloo.ca/journals/JIS/VOL29/Dohmen/dohmen4.tex The formula is attributed to J. Morgado (1972). It follows from ncard_regular_eq_sum_totient_unitaryDivisors; the filter spells out n.unitaryDivisors and keeps the source's shape.
Uses 1
Proof usesMorgado's formula as a sum over unitary divisors

TheoremMorgado's characterization of regular integers#●ready to prove

Let \(n\) be a positive integer and \(m\) an integer, and write \(\gcd\) for the nonnegative greatest common divisor. The congruence \(m^2 x \equiv m \pmod{n}\) has a solution \(x \in \mathbb{Z}\) if and only if \(\gcd(m^2, n) = \gcd(m, n)\), and \(\gcd(m^2, n) = \gcd(m, n)\) holds if and only if \(\gcd(m, n)\) and \(n / \gcd(m, n)\) are coprime, that is, \(\gcd(m, n)\) is a unitary divisor of \(n\).

theorem_wanted isRegularMod_iff_gcd_sq_eq_gcd {n : ℕ} (hn : 0 < n) (m : ℤ) :
    ((∃ x : ℤ, m ^ 2 * x ≡ m [ZMOD (n : ℤ)])
      ↔ Nat.gcd (m.natAbs ^ 2) n = Nat.gcd m.natAbs n)
    ∧ (Nat.gcd (m.natAbs ^ 2) n = Nat.gcd m.natAbs n
      ↔ Nat.Coprime (Nat.gcd m.natAbs n) (n / Nat.gcd m.natAbs n))
Sources
2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.