Revision #2996 → #3539 · back to history
c6ba592c2cde| Field | From #2996 | To #3539 |
|---|---|---|
| mathlib.decl | Nat.Prime.irrational_sqrt | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.Analysis.Transcendental.EIsTranscendental | — |
| note | Irrationality of e is available in Mathlib as a consequence of transcendence; searched-for `Irrational_exp_one`-style lemma exists via `Real.transcendental_exp_one` → irrational. | Previous mathlib pointer `Nat.Prime.irrational_sqrt` was unrelated (it concerns √p for prime p). Irrationality of e would follow from the (not-yet-fully-formalized) transcendence of e; no direct `Irrational (Real.exp 1)` declaration was verified. |
| status | formalized | not_formalized |
f4d4d3f030c1140b157a3494b7d24223c54fe6536d0fccc2