Lumenary.ElementaryNumberTheory

Formal library

• units_cyclictheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- For a prime `p`, the group `(ℤ/pℤ)ˣ` is cyclic: a primitive root exists. Mathlib proves
  that every finite subgroup of the units of an integral domain is cyclic
  (`isCyclic_of_subgroup_isDomain`), by the counting argument of the lesson. -/
  theorem units_cyclic (p : ℕ) [Fact p.Prime] : IsCyclic (ZMod p)ˣ :=
    inferInstance

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• sum_totienttheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- Gauss's identity `∑_{d ∣ n} φ(d) = n`, the key to the cyclicity proof. Mathlib's
  `Nat.sum_totient`. -/
  theorem sum_totient (n : ℕ) : ∑ d ∈ n.divisors, Nat.totient d = n :=
    Nat.sum_totient n

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• three_primitive_root_mod_seventheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- `3` is a primitive root modulo `7`: its powers `3, 2, 6, 4, 5, 1` run through all six
  non-zero residues, i.e. its order is `6`. `decide` checks `3⁶ = 1` and `3ᵐ ≠ 1` for `0 < m < 6`. -/
  theorem three_primitive_root_mod_seven : orderOf (3 : ZMod 7) = 6 :=
    (orderOf_eq_iff (by norm_num)).mpr ⟨by decide, by decide⟩

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• units_mod_eight_sqtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- Every unit modulo `8` squares to `1`: `1² = 1`, `3² = 9`, `5² = 25`, `7² = 49` are all `≡ 1`.
  Checked by `decide` over the four units. -/
  theorem units_mod_eight_sq : ∀ u : (ZMod 8)ˣ, u ^ 2 = 1 := by
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• no_primitive_root_mod_eighttheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **There is no primitive root modulo `8`.** `(ℤ/8ℤ)ˣ` has `φ(8) = 4` elements; a generator
  would have order `4`, but every unit has order dividing `2` (`units_mod_eight_sq`). -/
  theorem no_primitive_root_mod_eight : ¬ IsCyclic (ZMod 8)ˣ := by
    intro h
    obtain ⟨g, hg⟩ := h.exists_generator
    have hcard : Nat.card (ZMod 8)ˣ = 4 := by
      rw [Nat.card_eq_fintype_card, ZMod.card_units_eq_totient]
      decide
    have hord : orderOf g = 4 := by
      rw [← hcard]
      exact orderOf_eq_card_of_forall_mem_zpowers hg
    have hdvd : orderOf g ∣ 2 := orderOf_dvd_of_pow_eq_one (units_mod_eight_sq g)
    rw [hord] at hdvd
    omega

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• two_not_square_mod_fivetheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- `2` is a quadratic non-residue modulo `5`: the squares modulo `5` are `0, 1, 4`. -/
  theorem two_not_square_mod_five : ¬ IsSquare (2 : ZMod 5) := by
    rintro ⟨r, hr⟩
    revert hr
    revert r
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• euler_criteriontheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Euler's criterion**: for `a ≢ 0 (mod p)`, `a` is a square modulo `p` iff
  `a^((p − 1)/2) ≡ 1`. Mathlib's `ZMod.euler_criterion` (here `p / 2 = (p − 1)/2` for odd `p`). -/
  theorem euler_criterion (p : ℕ) [Fact p.Prime] {a : ZMod p} (ha : a ≠ 0) :
      IsSquare a ↔ a ^ (p / 2) = 1 :=
    ZMod.euler_criterion p ha

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• neg_one_square_ifftheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **First supplementary law**: `−1` is a square modulo a prime `p` iff `p ≢ 3 (mod 4)`.
  Mathlib's `ZMod.exists_sq_eq_neg_one_iff`. -/
  theorem neg_one_square_iff (p : ℕ) [Fact p.Prime] : IsSquare (-1 : ZMod p) ↔ p % 4 ≠ 3 :=
    ZMod.exists_sq_eq_neg_one_iff

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• two_square_ifftheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Second supplementary law**: for an odd prime `p`, `2` is a square modulo `p` iff
  `p ≡ ±1 (mod 8)`. Mathlib's `ZMod.exists_sq_eq_two_iff`. -/
  theorem two_square_iff (p : ℕ) [Fact p.Prime] (hp : p ≠ 2) :
      IsSquare (2 : ZMod p) ↔ p % 8 = 1 ∨ p % 8 = 7 :=
    ZMod.exists_sq_eq_two_iff hp

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• quadratic_reciprocitytheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **The law of quadratic reciprocity**: for distinct odd primes `p` and `q`,
  `(q/p)(p/q) = (−1)^(((p−1)/2)((q−1)/2))`. Mathlib's `legendreSym.quadratic_reciprocity`,
  proved (like the lesson) via Gauss's lemma and a lattice-point count. -/
  theorem quadratic_reciprocity (p q : ℕ) [Fact p.Prime] [Fact q.Prime] (hp : p ≠ 2) (hq : q ≠ 2)
      (hpq : p ≠ q) :
      legendreSym q p * legendreSym p q = (-1) ^ (p / 2 * (q / 2)) :=
    legendreSym.quadratic_reciprocity hp hq hpq

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• moebius_inversiontheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Möbius inversion**: `g(n) = ∑_{d ∣ n} f(d)` for all `n > 0` iff
  `f(n) = ∑_{de = n} μ(d) g(e)` for all `n > 0`. Mathlib's
  `ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq`. -/
  theorem moebius_inversion {f g : ℕ → ℤ} :
      (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔
        ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal,
          (ArithmeticFunction.moebius x.fst : ℤ) * g x.snd = f n :=
    ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• sq_mod_fourtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- Squares modulo `4` are `0` or `1`. -/
  theorem sq_mod_four : ∀ x : ZMod 4, x ^ 2 = 0 ∨ x ^ 2 = 1 := by
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• not_sum_two_squarestheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- No integer `≡ 3 (mod 4)` is a sum of two squares: modulo `4`, `a² + b²` is `0 + 0`, `0 + 1`,
  `1 + 0` or `1 + 1`, never `3`. In particular no prime `p ≡ 3 (mod 4)` is a sum of two squares. -/
  theorem not_sum_two_squares (a b : ℤ) : (a ^ 2 + b ^ 2) % 4 ≠ 3 := by
    intro h
    have hcast : ((a ^ 2 + b ^ 2 : ℤ) : ZMod 4) = ((3 : ℤ) : ZMod 4) := by
      rw [ZMod.intCast_eq_intCast_iff']
      simpa using h
    push_cast at hcast
    rcases sq_mod_four (a : ZMod 4) with ha | ha <;> rcases sq_mod_four (b : ZMod 4) with hb | hb <;>
      rw [ha, hb] at hcast <;> revert hcast <;> decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• brahmagupta_fibonaccitheoremProved here from basic factspropext, Quot.sound

  /-- **Brahmagupta–Fibonacci identity**: a product of sums of two squares is a sum of two squares,
  `(a² + b²)(c² + d²) = (ac − bd)² + (ad + bc)²` — the multiplicativity of the norm on `ℤ[i]`. -/
  theorem brahmagupta_fibonacci (a b c d : ℤ) :
      (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2 := by
    ring

  Axioms used: propext, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• fermat_two_squarestheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Fermat's two-squares theorem**: a prime `p` with `p ≢ 3 (mod 4)` is a sum of two squares.
  Mathlib's `Nat.Prime.sq_add_sq`, proved via the Gaussian integers as in the lesson. -/
  theorem fermat_two_squares (p : ℕ) [Fact p.Prime] (hp : p % 4 ≠ 3) :
      ∃ a b : ℕ, a ^ 2 + b ^ 2 = p :=
    Nat.Prime.sq_add_sq hp

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• pell_compositiontheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Composition of Pell solutions** (Brahmagupta's *bhāvanā*): if `x₁² − d y₁² = 1` and
  `x₂² − d y₂² = 1`, then `(x₁x₂ + d y₁y₂)² − d (x₁y₂ + x₂y₁)² = 1`. It is the multiplicativity of
  the norm `N(x + y√d) = x² − dy²`. -/
  theorem pell_composition (d x₁ y₁ x₂ y₂ : ℤ) (h₁ : x₁ ^ 2 - d * y₁ ^ 2 = 1)
      (h₂ : x₂ ^ 2 - d * y₂ ^ 2 = 1) :
      (x₁ * x₂ + d * y₁ * y₂) ^ 2 - d * (x₁ * y₂ + x₂ * y₁) ^ 2 = 1 := by
    linear_combination (x₂ ^ 2 - d * y₂ ^ 2) * h₁ + h₂

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• pell_thirteentheoremProved here from basic factspropext

  /-- The fundamental solution of `x² − 13y² = 1` is surprisingly large: `649² − 13 · 180² = 1`. -/
  theorem pell_thirteen : (649 : ℤ) ^ 2 - 13 * 180 ^ 2 = 1 := by
    norm_num

  Axioms used: propextformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• pell_existstheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Pell's equation has a non-trivial solution** for every positive non-square `d`.
  Mathlib's `Pell.exists_of_not_isSquare`, proved by Dirichlet's approximation argument as in the
  lesson. -/
  theorem pell_exists {d : ℤ} (h₀ : 0 < d) (hd : ¬ IsSquare d) :
      ∃ x y : ℤ, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0 :=
    Pell.exists_of_not_isSquare h₀ hd

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

• pell_powerstheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- Every solution with `x > 0` and `y ≥ 0` is a power of the fundamental solution `ε`:
  `x + y√d = εⁿ`. Mathlib's `Pell.IsFundamental.eq_pow_of_nonneg`, stated for its structure
  `Pell.Solution₁ d` of solutions. -/
  theorem pell_powers {d : ℤ} {ε : Pell.Solution₁ d} (hε : Pell.IsFundamental ε)
      {a : Pell.Solution₁ d} (hx : 0 < a.x) (hy : 0 ≤ a.y) : ∃ n : ℕ, a = ε ^ n :=
    hε.eq_pow_of_nonneg hx hy

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ElementaryNumberTheory.leanTry it in the Lean web editor

Formal exercises

Each exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.

/-- Two solutions of Pell's equation compose to a third.
Hint: the left side minus `1` equals `(x₂² − d y₂²)(x₁² − d y₁² − 1) + (x₂² − d y₂² − 1)`;
`linear_combination` can use `h₁` and `h₂` with polynomial coefficients. -/
theorem pell_composition (d x₁ y₁ x₂ y₂ : ℤ) (h₁ : x₁ ^ 2 - d * y₁ ^ 2 = 1)
    (h₂ : x₂ ^ 2 - d * y₂ ^ 2 = 1) :
    (x₁ * x₂ + d * y₁ * y₂) ^ 2 - d * (x₁ * y₂ + x₂ * y₁) ^ 2 = 1 := by
  sorry

/-- **Composition of Pell solutions** (Brahmagupta's *bhāvanā*): if `x₁² − d y₁² = 1` and
`x₂² − d y₂² = 1`, then `(x₁x₂ + d y₁y₂)² − d (x₁y₂ + x₂y₁)² = 1`. It is the multiplicativity of
the norm `N(x + y√d) = x² − dy²`. -/
theorem pell_composition (d x₁ y₁ x₂ y₂ : ℤ) (h₁ : x₁ ^ 2 - d * y₁ ^ 2 = 1)
    (h₂ : x₂ ^ 2 - d * y₂ ^ 2 = 1) :
    (x₁ * x₂ + d * y₁ * y₂) ^ 2 - d * (x₁ * y₂ + x₂ * y₁) ^ 2 = 1 := by
  linear_combination (x₂ ^ 2 - d * y₂ ^ 2) * h₁ + h₂

/-- There is no primitive root modulo 8.
Hint: a generator `g` would have `orderOf g = 4` (`orderOf_eq_card_of_forall_mem_zpowers`), but
`units_mod_eight_sq g` shows `g ^ 2 = 1`, so `orderOf g ∣ 2`. -/
theorem no_primitive_root_mod_eight : ¬ IsCyclic (ZMod 8)ˣ := by
  sorry

/-- **There is no primitive root modulo `8`.** `(ℤ/8ℤ)ˣ` has `φ(8) = 4` elements; a generator
would have order `4`, but every unit has order dividing `2` (`units_mod_eight_sq`). -/
theorem no_primitive_root_mod_eight : ¬ IsCyclic (ZMod 8)ˣ := by
  intro h
  obtain ⟨g, hg⟩ := h.exists_generator
  have hcard : Nat.card (ZMod 8)ˣ = 4 := by
    rw [Nat.card_eq_fintype_card, ZMod.card_units_eq_totient]
    decide
  have hord : orderOf g = 4 := by
    rw [← hcard]
    exact orderOf_eq_card_of_forall_mem_zpowers hg
  have hdvd : orderOf g ∣ 2 := orderOf_dvd_of_pow_eq_one (units_mod_eight_sq g)
  rw [hord] at hdvd
  omega