Documentation

FormalConjectures.Wikipedia.RegularPrimes

Infinite Regular Primes #

We define the notion of regular primes, which are prime numbers that are coprime with the cardinality of the class group of the p-th cyclotomic field. We also state that there are infinitely many regular primes.

Reference: Wikipedia

source
noncomputable def RegularPrimes.IsRegularPrime (p : ℕ) [Fact (Nat.Prime p)] :
Prop

A natural prime number p is regular if p is coprime with the order of the class group of the p-th cyclotomic field.

Equations
Instances For
    source
    theorem RegularPrimes.not_isRegularPrime_37_first :
    ¬IsRegularPrime 37

    The prime 37 is not a regular prime.

    source
    def RegularPrimes.regularPrimes :
    Set ℕ

    The set of regular primes.

    Equations
    Instances For
      source
      def RegularPrimes.irregularPrimes :
      Set ℕ

      The set of irregular primes.

      Equations
      Instances For
        source
        theorem RegularPrimes.small_regular_primes :
        {2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31} ⊆ regularPrimes

        The primes 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, and 31 are regular.

        source
        theorem RegularPrimes.not_isRegularPrime_37_second :
        ¬IsRegularPrime 37

        The prime 37 is not a regular prime.

        source
        theorem RegularPrimes.isRegularPrime_iff_Bernoulli (p : ℕ) [Fact (Nat.Prime p)] :
        IsRegularPrime p ↔ ∀ k ∈ Finset.Icc 2 (p - 3), ¬↑p ∣ (bernoulli' k).num

        An equivanlent definitions of regualr prime p is that it does not divide the numerator of the first p-3 Bernoulli numbers. Not in Mathlib.

        source
        theorem RegularPrimes.infinitude_of_irregularprimes :
        irregularPrimes.Infinite

        The set of irregular primes is infinite.

        source
        def RegularPrimes.RegularPrimeConjecture :
        Prop

        Conjecture: The set of regular primes is infinite.

        Equations
        Instances For
          source
          theorem RegularPrimes.regularprime_conjecture :
          RegularPrimeConjecture

          Conjecture: The set of regular primes is infinite.