Revision #1434 → #1848 · back to history
addedGaussian integers (Gauss)f555f708388e
addedRoots of unity / cyclotomic fields5f68fb3b93f1
modifiedPrime number (historical)1540c5a58299
| Field | From #1434 | To #1848 |
|---|
| mathlib.module | Mathlib.Data.Nat.Prime.Basic | Mathlib.Data.Nat.Prime.Defs |
addedEuclidean algorithm (gcd)c619eeb16fb7
modifiedPrime number theorem49a5c53fb798
| Field | From #1434 | To #1848 |
|---|
| mathlib.module | Mathlib.NumberTheory.Chebyshev | Mathlib.NumberTheory.PrimeCounting |
| note | Chebyshev-style bounds are formalized but the full PNT asymptotic π(x) ~ x/log x is not in Mathlib. | The prime-counting function `π(x)` is defined and Chebyshev-style bounds exist, but the full PNT asymptotic π(x) ~ x/log x is not in Mathlib. |
modifiedIntegers form a ringb7b14d257450
| Field | From #1434 | To #1848 |
|---|
| mathlib.module | Mathlib.Data.Int.Defs | Mathlib.Algebra.Ring.Int.Defs |
modifiedRational number1c2aa84c8da9
| Field | From #1434 | To #1848 |
|---|
| mathlib.module | Init.Data.Rat | Init.Data.Rat.Basic |
modifiedEqual fractions example22126c13035a
| Field | From #1434 | To #1848 |
|---|
| mathlib.decl | Rat.mk_pnat | mkRat |
| mathlib.module | Mathlib.Data.Rat.Defs | Init.Data.Rat.Basic |
| note | Mathlib normalizes rationals so equal fractions yield the same `Rat`, but no specific example lemma exists. | The smart constructor `mkRat` normalizes by gcd so different fractions reduce to the same `Rat`; no specific example lemma is stated. |
modifiedLeast upper bound property087f21beaee3
| Field | From #1434 | To #1848 |
|---|
| mathlib.module | Mathlib.Data.Real.Archimedean | Mathlib.Algebra.Order.Archimedean.Real.Basic |
modifiedPurely imaginary number83952d68b179
| Field | From #1434 | To #1848 |
|---|
| label | Imaginary / Gaussian integer | Purely imaginary number |
| mathlib.decl | GaussianInt | Complex.re |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.NumberTheory.Zsqrtd.GaussianInt | Mathlib.Data.Complex.Basic |
| note | Gaussian integers are `Zsqrtd (-1)`; purely imaginary numbers correspond to `Complex.re = 0`. | No dedicated `IsPurelyImaginary` predicate in Mathlib; expressed as `z.re = 0`. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
addedGaussian integer6714faec3fec
modifiedPrime numberba2ae97186e7
| Field | From #1434 | To #1848 |
|---|
| mathlib.module | Mathlib.Data.Nat.Prime.Basic | Mathlib.Data.Nat.Prime.Defs |
addedBernoulli numbers7f89fe6502ae
addedFibonacci numbers42cc40947d49
addedPerfect numbers59951ded7359
modifiedAlgebraic integer8ffad9db1078
| Field | From #1434 | To #1848 |
|---|
| mathlib.module | Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic | Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs |
modifiedOrdinal and cardinal numbers25f1d6bed54e
| Field | From #1434 | To #1848 |
|---|
| note | Both `Ordinal` and `Cardinal` (Mathlib.SetTheory.Cardinal.Basic) are formalized. | Both `Ordinal` and `Cardinal` (Mathlib.SetTheory.Cardinal.Defs) are formalized. |
addedCardinal numbere651c1fcd59a
modifiedSuperreal and surreal numbersdd67f4bda95e
| Field | From #1434 | To #1848 |
|---|
| note | Neither superreal nor surreal numbers are defined in Mathlib. | Neither superreal nor surreal numbers are currently in Mathlib (no `Surreal` or `SetTheory/Surreal` files exist). |
| provenance | ai | ai-moderated |