8.4. The final theorem🔗

Theorem8.4.1

uses 1used by 1✓L∃∀N

Kummer's criterion. Let p be an odd prime. Then \mathrm{IsRegularPrime}(p) \quad\Longleftrightarrow\quad \forall k,\ 1\le k,\ 2k\le p-3,\quad p\nmid (B_{2k})_{\mathrm{num}}.

Theorem 8.3.2

Lean code for Theorem8.4.1●1 theorem

theoremdefined in BernoulliRegular/Main.lean

complete

theorem BernoulliRegular.KummerCriterion {p : ℕ} [hp : Fact (Nat.Prime p)]
  (hp_odd : p ≠ 2) :
  IsRegularPrime p ↔
    ∀ (k : ℕ), 1 ≤ k → 2 * k ≤ p - 3 → ¬↑p ∣ (bernoulli (2 * k)).num

theorem BernoulliRegular.KummerCriterion {p : ℕ}
  [hp : Fact (Nat.Prime p)]
  (hp_odd : p ≠ 2) :
  IsRegularPrime p ↔
    ∀ (k : ℕ),
      1 ≤ k →
        2 * k ≤ p - 3 →
          ¬↑p ∣ (bernoulli (2 * k)).num

**Kummer's criterion.**

An odd prime `p` is regular iff `p` does not divide the numerator of any
Bernoulli number `B_2, B_4, ..., B_{p-3}`.

Proof for Theorem 8.4.1

uses 0

Take K to be the standard cyclotomic field K=\mathbb{Q}(\zeta_p). By definition, regularity of p is coprimality with the class number of this standard cyclotomic field. Since p is prime, this is equivalent to \neg\, p\mid h(\mathbb{Q}(\zeta_p)). Applying Theorem 8.3.2 to this K identifies divisibility by p with the existence of a Bernoulli numerator in Kummer's range divisible by p. Negating \exists k,\ 1\le k,\ 2k\le p-3,\quad p\mid (B_{2k})_{\mathrm{num}} gives exactly the displayed universal non-divisibility condition.