Prove2Me

The units of Z/mZ\mathbb{Z}/m\mathbb{Z} number φ(m)\varphi(m)

Proved
ShaoThreeUnits.card_units_filter

by aarontcao · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricsnumber-theory

The finite set of residues modulo mm that are units has exactly φ(m)\varphi(m) elements.

This is the bridge between the two ways of writing the density hypothesis of the main theorem. One side counts a Finset (ZMod m) and the other is Nat.totient m. Mathlib proves the group-theoretic form, that the unit group (Z/mZ)×(\mathbb{Z}/m\mathbb{Z})^\times has φ(m)\varphi(m) elements; what is wanted here is the same count for the Finset of unit residues that the other statements sum over.

Preamble
import Mathlib
open scoped Classical
Formal statement
namespace ShaoThreeUnits

theorem card_units_filter (m : ℕ) [NeZero m] :
    (Finset.univ.filter (fun x : ZMod m => IsUnit x)).card = Nat.totient m := by sorry

end ShaoThreeUnits
Source
Xuancheng Shao, "A density version of the Vinogradov three primes theorem", Duke Math. J. 163 (2014) 489-512, arXiv:1206.6139v2, https://arxiv.org/abs/1206.6139, used throughout Sections 1 and 3
Read-back

What the Lean code literally says, in plain math · claude-opus-5

READ-BACK

For every natural number m that is nonzero (the nonzero-ness enters as a typeclass, not as an explicit hypothesis), consider the ring of integers modulo m. It is a finite ring under this assumption, so one may form the finite set of all of its elements and select those elements that are invertible, meaning those x for which some y in the same ring satisfies x times y equal to 1. The claim is that the number of such invertible residues equals Euler's totient function at m, that is, the count of integers k in the range 0 to m minus 1 that are coprime to m. The statement is an equality of natural numbers, not an inequality or a bijection: it asserts the two counts agree exactly, for each fixed m separately. Nothing here is existentially quantified, no constant is left unnamed, and the equality is between a cardinality computed inside the ring and a purely arithmetic function of m. The declaration is stated with its proof omitted (the body is a placeholder), so the file asserts the statement without establishing it.

QUANTIFIER ORDER m, a natural number, universally quantified, scope is the whole equality. No other binder is quantified over at the statement level; the x inside the selection is the bound variable of the selection predicate, ranging over residues mod m.

HYPOTHESES Nonzero-ness of m (a typeclass constraint): rules out m = 0. This is load-bearing rather than cosmetic, since for m = 0 the ring of residues is the integers, which is infinite and admits no finiteness instance, so the left side would not even be well formed. It does not rule out m = 1. Invertibility of x (the selection predicate): keeps only those residues with a two-sided multiplicative inverse in the ring. Classical logic is switched on in scope, which supplies decidability for the selection predicate. It does not change which elements are selected.

DEGENERATE CASES m = 1: the ring of residues is the one-element ring, where 0 and 1 coincide, so the single element is invertible and the left side is 1. The totient of 1 is also 1, so the statement is a genuine (nonvacuous) assertion there. m = 0: excluded by the typeclass, as above; the identity would fail in spirit anyway since the totient of 0 is 0. m prime: both sides are m minus 1, no special-casing in the statement. The hypothesis set is satisfiable for every m at least 1, so the statement is not vacuous.

UNREADABLE Nothing. The payload contains one declaration and no auxiliary definitions, and every name in it is standard vocabulary.

Human review

  • Endorsed by Shuze Chen · Sep 17, 2026

  • Endorsed by aarontcao · Sep 17, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph