Revision #1364 → #2103 · back to history
modifiedLindemann–Weierstrass theorem798be804cfbf
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | LindemannWeierstrass.exp_polynomial_approx |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart |
| note | — | Only the analytic preparation lemma is in Mathlib; the main Lindemann–Weierstrass linear-independence statement is not formalized. |
| status | — | partial |
modifiedEquivalent formulation (Baker)96c7e22af0d0
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | LindemannWeierstrass.exp_polynomial_approx |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart |
| note | — | Equivalent to the main theorem; only the analytic preparation lemma exists, not the algebraic-independence/linear-independence conclusion. |
| status | — | partial |
modifiedTranscendence of e868d6f0fc5d6
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No declaration `Transcendental ℤ (Real.exp 1)` (or analogue) found in Mathlib via grep, loogle, or semantic search. |
| status | — | not_formalized |
modifiedTranscendence of e^α via second formulatione7b2d181e4e1
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Transcendence of e^α for algebraic α≠0 is not formalized; depends on the un-formalized main Lindemann–Weierstrass theorem. |
| status | — | not_formalized |
modifiedTranscendence of πb809dcbc3109
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | irrational_pi |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.Real.Pi.Irrational |
| note | — | Only irrationality of π is formalized (`irrational_pi`); transcendence of π is not in Mathlib. |
| status | — | partial |
modifiedTranscendence of sin, cos, tan of algebraic numbers5787e8b42ecf
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No declaration asserting transcendence of sin/cos/tan/sinh/cosh/tanh at nonzero algebraic arguments found in Mathlib. |
| status | — | not_formalized |
modifiedp-adic Lindemann–Weierstrass Conjecturebb5aca6b556a
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | p-adic version is an open conjecture; not stated or formalized in Mathlib. |
| status | — | not_formalized |
modifiedModular conjecture0f3fd0e12dc0
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The modular-j analogue conjecture is not stated in Mathlib. |
| status | — | not_formalized |
modifiedLindemann–Weierstrass Theorem (Baker's reformulation)6036f3fd82f2
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | LindemannWeierstrass.exp_polynomial_approx |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart |
| note | — | Baker's reformulation is not formalized; only the analytic approximation lemma is present. |
| status | — | partial |
modifiedLemma Ac27229085bf1
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | LindemannWeierstrass.exp_polynomial_approx |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart |
| note | — | Lemma A's analytic content is captured by `exp_polynomial_approx`, but the full propositional statement (no rational vanishing sum) is not formalized. |
| status | — | partial |
modifiedLemma B53b3d8c40e25
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | LindemannWeierstrass.exp_polynomial_approx |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart |
| note | — | Lemma B (with algebraic coefficients) is not formalized; only related analytic infrastructure exists. |
| status | — | partial |
modifiedLemma A implies e is irrationalfe5e64c0579e
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Irrationality of e via Lemma A is not present in Mathlib; no `irrational_exp_one` or equivalent was found. |
| status | — | not_formalized |
modifiedLemma A implies π is irrational2ac6e51ec897
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | irrational_pi |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.Real.Pi.Irrational |
| note | — | Mathlib has `irrational_pi`, but it is proved by Niven's method rather than as a consequence of Lemma A. |
| status | — | partial |
modifiedLemma B implies e is transcendental15ed8d49a194
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Transcendence of e (via Lemma B or otherwise) is not formalized in Mathlib. |
| status | — | not_formalized |
modifiedLemma B implies π is transcendental9049340211ce
| Field | From #1364 | To #2103 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Transcendence of π is not formalized in Mathlib (only irrationality is). |
| status | — | not_formalized |
addedTranscendence degree reformulationb8f6a7688d50
addedHermite's theorem (integer-exponent special case)f9435f175fe7