Different Proofs

1. Fermat's Little Theorem🔗

Definition1.1
Group: Fermat's Little Theorem. (10)
Group member previews
Preview
Definition 1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

Fermat's Little Theorem, in integer form, says that for any prime p and integer a, one has a^p \equiv a \pmod p.

Lean code for Definition1.1●1 definition
Definition1.2
Group: Fermat's Little Theorem. (10)
Group member previews
Preview
Definition 1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

The natural-number form says that for any prime p and natural number a, one has a^p \equiv a \pmod p.

Lean code for Definition1.2●1 definition
Theorem1.3
Group: Fermat's Little Theorem. (10)
Group member previews
Preview
Definition 1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 1.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The natural-number statement Definition 1.2 implies the integer statement Definition 1.1.

Lean code for Theorem1.3●1 theorem
  • theoremdefined in DifferentProofs/FermatLittleTheorem/Basic.lean
    complete
    theorem FermatLittleTheoremNat_impl_FermatLittleTheorem :
  FermatLittleTheoremNat → FermatLittleTheorem
    theorem FermatLittleTheoremNat_impl_FermatLittleTheorem :
  FermatLittleTheoremNat →
    FermatLittleTheorem
Proof for Theorem 1.3
uses 0

Work in \mathbb{Z}/p\mathbb{Z}. Every element is represented by the natural number ((a : ZMod p).val), so the natural-number congruence transfers back through the canonical map.

First proof uses the binomial theorem.

Theorem1.4
Group: Fermat's Little Theorem. (10)
Group member previews
Preview
Definition 1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

For any prime p and integer a, one has a^p \equiv a \pmod p.

Lean code for Theorem1.4●1 theorem
Proof for Theorem 1.4
uses 0

In characteristic p, Freshman's dream gives (x + 1)^p = x^p + 1. Applying this in ZMod p and inducting over natural representatives proves the congruence.

Second proof uses Lagrange's theorem on groups, applied to the multiplicative group of units in \mathbb{Z}/p\mathbb{Z}.

Theorem1.5
Group: Fermat's Little Theorem. (10)
Group member previews
Preview
Definition 1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

For any prime p and integer a, one has a^p \equiv a \pmod p.

Lean code for Theorem1.5●1 theorem
Proof for Theorem 1.5
uses 0

If a is zero modulo p, the claim is immediate. Otherwise a is a unit in \mathbb{Z}/p\mathbb{Z}; by Lagrange's theorem its order divides p - 1, so a^{p-1} = 1, and multiplying by a gives the result.

Third proof is by Alkauskas. It is based on a formal product expansion of a certain rational function, which is used to derive the natural-number form of Fermat's Little Theorem.

Lemma1.6
Group: Fermat's Little Theorem. (10)
Group member previews
Preview
Definition 1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

Let g \in \mathbb{Z}[[x]] be an integer power series of the form g(x) = 1 - x - d x^2 + \sum_{k \ge 3} b_k x^k. For every N, there is a sequence of integers (a_n)_{n \ge 1} with a_1 = 1 such that g agrees with \prod_{n=1}^{N}(1 - a_n x^n) in all coefficients of degree at most N.

Lean code for Lemma1.6●1 theorem
  • theoremdefined in DifferentProofs/FermatLittleTheorem/Alkauskas.lean
    complete
    theorem FermatLittleTheorem.Alkauskas.exists_intExpansion {g : PowerSeries ℤ}
  (hg0 : PowerSeries.constantCoeff g = 1)
  (hg1 : (PowerSeries.coeff 1) g = -1) (N : ℕ) :
  ∃ a,
    a 1 = 1 ∧
      ∀ k ≤ N,
        (PowerSeries.coeff k) g =
          (PowerSeries.coeff k)
            (∏ n ∈ Finset.Icc 1 N,
              (1 - PowerSeries.C (a n) * PowerSeries.X ^ n))
    theorem FermatLittleTheorem.Alkauskas.exists_intExpansion
  {g : PowerSeries ℤ}
  (hg0 : PowerSeries.constantCoeff g = 1)
  (hg1 : (PowerSeries.coeff 1) g = -1)
  (N : ℕ) :
  ∃ a,
    a 1 = 1 ∧
      ∀ k ≤ N,
        (PowerSeries.coeff k) g =
          (PowerSeries.coeff k)
            (∏ n ∈ Finset.Icc 1 N,
              (1 -
                PowerSeries.C (a n) *
                  PowerSeries.X ^ n))
Proof for Lemma 1.6
uses 0

Choose the factors inductively. Multiplying by 1 - a_{N+1}x^{N+1} leaves all lower coefficients fixed, and the integer a_{N+1} can be chosen to match the coefficient of x^{N+1}.

Theorem1.7
Group: Fermat's Little Theorem. (10)
Group member previews
Preview
Definition 1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

For any prime p and integer a, one has a^p \equiv a \pmod p.

Lean code for Theorem1.7●1 theorem
Proof for Theorem 1.7
Proof uses 2
Proof dependency previews
Preview
Theorem 1.3
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Apply the integer formal product expansion Lemma 1.6 to \frac{1-(d+1)x}{1-dx}. Comparing the coefficient of x^p in the negated logarithmic derivative gives p \mid (d+1)^p - d^p - 1. Telescoping these congruences over d proves the natural-number form, then the reduction Theorem 1.3 gives the integer form.

Fourth proof is by a dynamical argument, using the map T_n : [0,1] \to [0,1] defined by T_n(x) = \{nx\} for 0 \le x < 1 and T_n(1) = 1, and considering the fixed points of T_{a^p} that are not fixed by T_a.

Definition1.8
Group: Fermat's Little Theorem. (10)
Group member previews
Preview
Definition 1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 2
Reverse dependency previews
Preview
Lemma 1.9
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For a natural number n, define T_n : [0,1] \to [0,1] by T_n(x) = \{nx\} for 0 \le x < 1 and T_n(1) = 1.

Lean code for Definition1.8●1 definition
Lemma1.9
Group: Fermat's Little Theorem. (10)
Group member previews
Preview
Definition 1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

For natural numbers m and n, the maps satisfy T_m \circ T_n = T_{mn}. This is a consequence of Definition 1.8.

Lean code for Lemma1.9●1 theorem
  • theoremdefined in DifferentProofs/FermatLittleTheorem/Dynamical.lean
    complete
    theorem FermatLittleTheorem.Dynamical.T_comp_eq_mul (m n : ℕ) :
  FermatLittleTheorem.Dynamical.T m ∘
      FermatLittleTheorem.Dynamical.T n =
    FermatLittleTheorem.Dynamical.T (m * n)
    theorem FermatLittleTheorem.Dynamical.T_comp_eq_mul
  (m n : ℕ) :
  FermatLittleTheorem.Dynamical.T m ∘
      FermatLittleTheorem.Dynamical.T n =
    FermatLittleTheorem.Dynamical.T
      (m * n)
Proof for Lemma 1.9
uses 0

Away from 1, write fractional parts as subtraction of floors: \{m\{nx\}\} = \{mnx\} because the difference is an integer. The endpoint 1 is fixed by definition.

Lemma1.10
Group: Fermat's Little Theorem. (10)
Group member previews
Preview
Definition 1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

For any n \ge 2, the map T_n has exactly n fixed points. This counts the fixed points of Definition 1.8.

Lean code for Lemma1.10●1 theorem
  • theoremdefined in DifferentProofs/FermatLittleTheorem/Dynamical.lean
    complete
    theorem FermatLittleTheorem.Dynamical.T_num_fp_eq (n : ℕ) (hn : 2 ≤ n) :
  Nat.card ↑{x | FermatLittleTheorem.Dynamical.T n x = x} = n
    theorem FermatLittleTheorem.Dynamical.T_num_fp_eq
  (n : ℕ) (hn : 2 ≤ n) :
  Nat.card
      ↑{x |
          FermatLittleTheorem.Dynamical.T
              n x =
            x} =
    n
Proof for Lemma 1.10
uses 0

For x < 1, the equation T_n(x)=x is equivalent to (n-1)x \in \mathbb{Z}, giving the points j/(n-1) for 0 \le j \le n-2. Together with the endpoint 1, these are exactly n fixed points.

Theorem1.11
Group: Fermat's Little Theorem. (10)
Group member previews
Preview
Definition 1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

For any prime p and integer a, one has a^p \equiv a \pmod p. The proof uses Lemma 1.9, Lemma 1.10, and the reduction Theorem 1.3.

Lean code for Theorem1.11●1 theorem
Proof for Theorem 1.11
uses 1

By Theorem 1.3, it suffices to prove the natural-number form. It suffices to prove the natural-number form. For a \ge 2, consider the fixed points of T_{a^p} that are not fixed by T_a. Their cardinality is a^p-a, and the action of T_a partitions this set into orbits of size p, so p divides a^p-a.