Fermat's little theorem and the freshman's dream, for every prime

[Rafael-SOWNet]

Part of #1409.

This decides Sullivan and Mackey's Prob 8.9.25 and 8.9.26 for every prime, derived from #1500's p divides binomial(p, k) as the book derives them:

forall p in PP : forall a, b in ZZ : (a + b)^p = a^p + b^p (mod p)	True
forall p in PP : forall a in ZZ : a^p = a (mod p)	True
forall p in PP : forall a in ZZ : a^p mod p = a mod p	True

The freshman's dream

With p prime in scope, p divides d holds where replacing each power (u + v)^p in d by u^p + v^p leaves nothing, or only multiples of p. The binomial theorem adds binomial(p, k) u^k v^(p - k) for 0 < k < p, and #1500's rule says p divides each of those.

The rule asks the quantifiers forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k) before it answers, and records that as the step it rests on. It requires three things:

• d is a polynomial with whole coefficients, in quantities that are whole by the facts in scope;
• every atom in d is a p-th power of such a polynomial, so the congruence carries through products;
• a difference is read as u^p - v^p, since (-v)^p is -v^p modulo every prime, 2 included.

Congruentf reads the same rule.

Fermat's little theorem

This is a new route for forall x in S : f = g (mod m), or f mod m = g mod m, over ZZ, ZZ* or ZZ+, where m is a symbol that doesn't mention x. Write D for f - g.

• If m divides D at every member, the statement holds.
• Otherwise, suppose the statement holds at one member, and m divides D(x + 1) - D(x) at every member. Then D has one residue modulo m all along the row, up from that member and down from it, so the statement holds at every member.

For Fermat, the step is (a + 1)^p - (a + 1) - (a^p - a), which the freshman's dream reads. The base is at 1, since 0^p is only 0 provided p > 0.

Proof recording

    1 ^ p = 1 (mod p) is True: the base case, at 1, by evaluation [decide]
          p divides binomial(p, k) is True: p is prime and 0 < k < p, so p divides p! = binomial(p, k) k! (p - k)! and none of the factors of k! (p - k)! [Nat.Prime.dvd_choose_self]
        forall k in ZZ : 0 < k and k < p implies p divides binomial(p, k) is True: p divides binomial(p, k) holds for every k in ZZ with 0 < k and k < p [intro]
      p divides (a + 1) ^ p - (a + 1) - (a ^ p - a) is True: by the binomial theorem each (a + 1)^p is the sum of the p-th powers of its terms and multiples of p, and what is left of (a + 1) ^ p - (a + 1) - (a ^ p - a) is a multiple of p [add_pow_char]
    forall a in ZZ : p divides (a + 1) ^ p - (a + 1) - (a ^ p - a) is True: p divides the difference at a + 1 less the difference at a, at every member [intro]
  forall a in ZZ : a ^ p = a (mod p) is True: by induction up and down from 1: p divides the difference of the two sides there, and the difference changes by a multiple of p from each member to the next [Int.inductionOn']
forall p in PP : forall a in ZZ : a ^ p = a (mod p) is True: the body holds for every p in PP [intro]

The lemmas are add_pow_char (Mathlib/Algebra/CharP/Lemmas.lean), Int.inductionOn' and Int.modEq_iff_dvd : a ≡ b [ZMOD n] ↔ n ∣ b - a.

What else changes

A body is now renamed and decided with the facts in scope wherever it contains a divisibility, a congruence or an equation of residues by a modulus that isn't a number. In #1500 that happened only for p divides binomial(p, k). Statements with a numeric modulus are untouched.

Each of these fails as it should: over ZZ+ instead of the primes, with a + 1 on the right, or with + 1 added to the dream. (a + b)^p = a^p + b^p (mod p) on its own stays unevaluated after the quantified statement is decided.

Measured

Both were measured on this tree before the rebase onto #1500's merge, and the tree is unchanged by it.

• The unit suite passes on net10.0: 12749 passed, 14 skipped, none failed, out of 12763, of which 11 are new.
• The allocation gate passes on all 19 gated benchmarks.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura