Revision #1486 → #1852 · back to history
modifiedPrime number (lead)7cc1f7e0846e
| Field | From #1486 | To #1852 |
|---|
| note | `Nat.Prime` is defined as a natural number ≥ 2 not expressible as a product of smaller naturals. | `Nat.Prime` is the standard predicate for natural-number primality. |
modified5 is prime, 4 is composite0a82dfb49983
| Field | From #1486 | To #1852 |
|---|
| mathlib.module | Mathlib.Data.Nat.Prime.Basic | Mathlib.Data.Nat.Prime.Defs |
| note | Concrete primality facts like `Nat.prime_two`, `Nat.prime_three`, `Nat.prime_five` are present and `norm_num`'s `Prime` extension decides such examples. | Concrete primality facts like `Nat.prime_two` are available and `norm_num` decides such examples. |
modifiedFundamental theorem of arithmetic (lead)285b05bb6477
| Field | From #1486 | To #1852 |
|---|
| note | Existence and uniqueness of the prime factorization of naturals are formalized via `Nat.factors` and `UniqueFactorizationMonoid.factors_unique`. | Existence/uniqueness of prime factorization is formalized via `UniqueFactorizationMonoid.factors_unique` and `Nat.primeFactorsList_unique`. |
modifiedPrime number67e701f1c7d4
| Field | From #1486 | To #1852 |
|---|
| note | `Nat.Prime` is the standard predicate, equivalent to `Irreducible` on ℕ. | `Nat.Prime` is defined as irreducibility of a natural number ≥ 2. |
modifiedPrime via divisorse53aed2545de
| Field | From #1486 | To #1852 |
|---|
| note | Mathlib's `Nat.Prime` is defined via irreducibility, and the divisor-count characterization is implicit (e.g., `Nat.divisors_prime_pow`/`Nat.Prime.divisors`-style lemmas) rather than the literal definition. | Mathlib defines `Nat.Prime` via irreducibility, not directly via the two-divisors characterization, though related lemmas about `Nat.divisors` are available. |
modifiedPrimes among 1 through 6ae94c8eac82f
| Field | From #1486 | To #1852 |
|---|
| mathlib.module | Mathlib.Data.Nat.Prime.Basic | Mathlib.Data.Nat.Prime.Defs |
| note | `Nat.prime_two`, `Nat.prime_three`, `Nat.prime_five` and decidability of `Nat.Prime` (via `norm_num`) cover these examples. | `Nat.prime_two`, `Nat.prime_three`, `Nat.prime_five` plus decidability of `Nat.Prime` via `norm_num` cover these examples. |
modifiedFirst 25 prime numbers477eb03aea9f
| Field | From #1486 | To #1852 |
|---|
| mathlib.module | Mathlib.Data.Nat.PrimeFin | Mathlib.NumberTheory.PrimeCounting |
modifiedEvery prime > 2 is odd1ae8e4b81da2
| Field | From #1486 | To #1852 |
|---|
| note | `Nat.Prime.eq_two_or_odd'` proves that every prime equals 2 or is odd. | `Nat.Prime.eq_two_or_odd'` proves every prime equals 2 or is odd. |
modifiedWilson's theorem (history)f66b83bc5264
| Field | From #1486 | To #1852 |
|---|
| note | Wilson's theorem (`Nat.prime_iff_fac_equiv_neg_one`) characterizes primes via `(n-1)! ≡ -1 (mod n)`. | Wilson's theorem characterizes primes by `(n-1)! ≡ -1 (mod n)`. |
modifiedGoldbach's conjecture (history)bfe75818f02f
| Field | From #1486 | To #1852 |
|---|
| note | Goldbach's conjecture on sums of two primes is not stated in Mathlib (only Goldbach's coprimality theorem for Fermat numbers appears). | Goldbach's conjecture on sums of two primes is not stated in Mathlib. |
modifiedBertrand's postulatee916d47d486a
| Field | From #1486 | To #1852 |
|---|
| note | Bertrand's postulate is proved in `Mathlib.NumberTheory.Bertrand`. | Bertrand's postulate is proved as `Nat.bertrand` in `Mathlib.NumberTheory.Bertrand`. |
modifiedPrime number theorem (history)6059ec173e5c
| Field | From #1486 | To #1852 |
|---|
| mathlib.decl | Nat.Chebyshev.eventually_primeCounting_le | Chebyshev.eventually_primeCounting_le |
| note | The full PNT is not yet in Mathlib; only Chebyshev-type asymptotic bounds on π and the related ψ/θ functions are formalized. | Only Chebyshev-type upper bounds on π and related ψ/θ asymptotics are in Mathlib; the full PNT is not yet formalized. |
modifiedDirichlet's theorem on arithmetic progressions (history)89de87ad2056
| Field | From #1486 | To #1852 |
|---|
| mathlib.decl | Nat.setOf_prime_and_eq_mod_infinite | Nat.infinite_setOf_prime_and_eq_mod |
| note | Dirichlet's theorem on primes in arithmetic progressions is proved in `Mathlib.NumberTheory.LSeries.PrimesInAP`. | Dirichlet's theorem on primes in arithmetic progressions is `Nat.infinite_setOf_prime_and_eq_mod`. |
modifiedPrime factorization6c3ee5999b49
| Field | From #1486 | To #1852 |
|---|
| note | `Nat.factorization` gives a number's prime factorization as a finsupp; `Nat.primeFactorsList` provides the list of prime factors. | `Nat.factorization` gives a number's prime factorization as a finsupp; `Nat.primeFactorsList` returns the list of prime factors. |
modifiedPrime factors292b86349ece
| Field | From #1486 | To #1852 |
|---|
| mathlib.module | Mathlib.Data.Nat.Factorization.Defs | Mathlib.Data.Nat.PrimeFin |
| note | `Nat.primeFactors` and `Nat.primeFactorsList` give the set/list of prime factors of a natural number. | `Nat.primeFactors` (as a `Finset`) and `Nat.primeFactorsList` give the prime factors of a natural number. |
modifiedFundamental theorem of arithmetic216cdb288f8a
| Field | From #1486 | To #1852 |
|---|
| note | Existence/uniqueness of prime factorization in ℕ follows from `UniqueFactorizationMonoid` infrastructure; Mathlib explicitly proves `Nat.primeFactorsList_unique` etc. | Existence/uniqueness of prime factorization in ℕ is provided via the `UniqueFactorizationMonoid` infrastructure. |
modifiedEuclid's lemma1a4b6efdf3c8
| Field | From #1486 | To #1852 |
|---|
| mathlib.module | Mathlib.Data.Nat.Prime.Basic | Mathlib.Data.Nat.Prime.Defs |
modifiedEuclid numbers74abb7b5c11f
| Field | From #1486 | To #1852 |
|---|
| note | Euclid numbers (primorial + 1) are not named in Mathlib, though `Nat.primorial` exists. | Euclid numbers (primorial + 1) have no dedicated definition in Mathlib, though `Nat.primorial` exists. |
modifiedPrime number theorem90e613e16574
| Field | From #1486 | To #1852 |
|---|
| note | The asymptotic statement π(n) ~ n/log n is not yet formalized in Mathlib; only Chebyshev-type bounds appear. | The asymptotic π(n) ~ n/log n is not yet formalized in Mathlib; only Chebyshev-type bounds appear. |
modifiedOffset logarithmic integral estimate651ca849017e
| Field | From #1486 | To #1852 |
|---|
| note | The offset logarithmic integral and its asymptotic for π(n) are not in Mathlib. | The offset logarithmic integral Li(n) and its asymptotic for π(n) are not in Mathlib. |
modifiedArithmetic progressione1954b75240c
| Field | From #1486 | To #1852 |
|---|
| mathlib.decl | Finset.image | — |
| note | Mathlib has no dedicated `ArithmeticProgression` type; APs are encoded via `fun n ↦ a + n • d` ad hoc (e.g., in `Combinatorics.Additive.AP`). | Mathlib has no dedicated `ArithmeticProgression` type; APs are encoded ad hoc as `fun n ↦ a + n • d`. |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |
modifiedDirichlet's theorem on arithmetic progressionsfa02a424363e
| Field | From #1486 | To #1852 |
|---|
| mathlib.decl | Nat.setOf_prime_and_eq_mod_infinite | Nat.infinite_setOf_prime_and_eq_mod |
| note | Dirichlet's theorem on infinitely many primes in arithmetic progressions is in `Mathlib.NumberTheory.LSeries.PrimesInAP`. | Dirichlet's theorem on infinitely many primes in arithmetic progressions is `Nat.infinite_setOf_prime_and_eq_mod`. |
modifiedModular arithmetic5a7b387d8a25
| Field | From #1486 | To #1852 |
|---|
| mathlib.module | Mathlib.Data.ZMod.Basic | Mathlib.Data.ZMod.Defs |
modifiedModular arithmetic is a field iff modulus is prime0f578e9f016c
| Field | From #1486 | To #1852 |
|---|
| note | `ZMod p` is given a `Field` instance when `p` is prime. | `ZMod p` carries a `Field` instance when `p` is prime. |
modifiedp-adic order126bd30ea42f
| Field | From #1486 | To #1852 |
|---|
| mathlib.module | Mathlib.NumberTheory.Padics.PadicVal.Defs | Mathlib.Data.Nat.MaxPowDiv |
addedp-adic absolute valuecb7f0590891b
addedp-adic numbers (completion of ℚ)986ec8e0c378
modifiedOstrowski's theorem846816e49575
| Field | From #1486 | To #1852 |
|---|
| note | Ostrowski's theorem for ℚ is proved in `Mathlib.NumberTheory.Ostrowski`. | Ostrowski's theorem for ℚ is `Rat.AbsoluteValue.equiv_real_or_padic`. |
modifiedSpectrum of a ring02df4412a4de
| Field | From #1486 | To #1852 |
|---|
| note | `PrimeSpectrum R` is defined as the type of prime ideals of `R`. | `PrimeSpectrum R` is the type of prime ideals of `R`. |
addedQuadratic reciprocity5c33829cac4f
addedRegular primes18d3ef78366c
modifiedTrial division2ff400e8ebff
| Field | From #1486 | To #1852 |
|---|
| note | `Nat.minFac` finds the smallest prime factor by trial division; this serves as Mathlib's primality algorithm but `trial division` is not named. | `Nat.minFac` finds the smallest prime factor via trial division, but `trial division` itself is not a named algorithm. |
modifiedPseudoprimed5c2c980a907
| Field | From #1486 | To #1852 |
|---|
| mathlib.match_kind | exact | special_case |
| note | `Nat.FermatPsp` formalizes Fermat pseudoprimes. | Mathlib formalizes `Nat.FermatPsp` (Fermat pseudoprimes), a special case of the general pseudoprime notion; no generic `Pseudoprime` predicate parameterized by a test exists. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
modifiedFermat primescd67b57107b4
| Field | From #1486 | To #1852 |
|---|
| note | `Nat.fermatNumber` is defined but there is no dedicated `FermatPrime` predicate; one can write `(Nat.fermatNumber n).Prime`. | `Nat.fermatNumber` is defined but there is no dedicated `FermatPrime` predicate; one writes `(Nat.fermatNumber n).Prime`. |