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
instance RegularPrimes.instNumberFieldCyclotomicFieldMkNatLtOfNatRat_formalConjectures (p : ℕ) [hp : Fact (Nat.Prime p)] :
NumberField (CyclotomicField ⟨p, ⋯⟩ ℚ)

TODO: remove this once mathlib is updated as it seems that in this version of mathlib we need to do this manually.

source
def RegularPrimes.IsRegularPrime (p : ℕ) [hp : 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
    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
        source
        theorem RegularPrimes.not_isRegularPrime_37_second :
        ¬IsRegularPrime 37
        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.