/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilInfinite 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.
open scoped NumberField
variable (p : ℕ)
namespace RegularPrimes
A natural prime number p is regular if p is coprime with the order of the class group
of the p-th cyclotomic field.
noncomputable def IsRegularPrime [Fact p.Prime] : Prop :=
p.Coprime <| Fintype.card <| ClassGroup (𝓞 <| CyclotomicField p ℚ)The prime 37 is not a regular prime.
@[category textbook, AMS 11]
theorem not_isRegularPrime_37_first : ¬ @IsRegularPrime 37 (p:ℕ⊢ Fact (Nat.Prime 37) All goals completed! 🐙) := ⊢ ¬IsRegularPrime 37
All goals completed! 🐙The set of regular primes.
def regularPrimes : Set ℕ := { p | ∃ (hp : Nat.Prime p), @IsRegularPrime p ⟨hp⟩ }The set of irregular primes.
def irregularPrimes : Set ℕ := { p | ∃ (hp : Nat.Prime p), ¬ @IsRegularPrime p ⟨hp⟩ }The primes 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, and 31 are regular.
@[category textbook, AMS 11]
lemma small_regular_primes :
{ 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31 } ⊆ regularPrimes := ⊢ {2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31} ⊆ regularPrimes
All goals completed! 🐙The prime 37 is not a regular prime.
@[category textbook, AMS 11]
theorem not_isRegularPrime_37_second : ¬ @IsRegularPrime 37 (p:ℕ⊢ Fact (Nat.Prime 37) All goals completed! 🐙) := ⊢ ¬IsRegularPrime 37
All goals completed! 🐙
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.
@[category textbook, AMS 11]
theorem isRegularPrime_iff_Bernoulli (p : ℕ) [Fact p.Prime] :
IsRegularPrime p ↔ ∀ k ∈ Finset.Icc 2 (p - 3), ¬ (p : ℤ) ∣ (bernoulli' k).num := p:ℕinst✝:Fact (Nat.Prime p)⊢ IsRegularPrime p ↔ ∀ k ∈ Finset.Icc 2 (p - 3), ¬↑p ∣ (bernoulli' k).num
All goals completed! 🐙The set of irregular primes is infinite.
@[category research solved, AMS 11]
theorem infinitude_of_irregularprimes : irregularPrimes.Infinite := ⊢ irregularPrimes.Infinite
All goals completed! 🐙Conjecture: The set of regular primes is infinite.
def RegularPrimeConjecture : Prop :=
regularPrimes.InfiniteConjecture: The set of regular primes is infinite.
@[category research open, AMS 11]
theorem regularprime_conjecture : RegularPrimeConjecture := ⊢ RegularPrimeConjecture
All goals completed! 🐙
end RegularPrimes