Revision #3356 → #3889 · back to history
addedPythagorean theorem0173deeed48e
addedAlgebraic numberdcbc1e222b94
modifiede is irrational and transcendental6bd92c4db138
| Field | From #3356 | To #3889 |
|---|
| note | Neither irrationality nor transcendence of `Real.exp 1` is recorded under any obvious name in Mathlib (`irrational_e` and `transcendental_e` do not exist). | Neither irrationality nor transcendence of `Real.exp 1` is formalized in Mathlib (no `Complex.transcendental_e`, `irrational_exp_one`, or equivalent lemma exists). |
| provenance | ai | ai-moderated |
addedGolden ratioff6145c71ab3
modifiedKepler: φ as limit of Fibonacci ratios1a91ccd8bf44
| Field | From #3356 | To #3889 |
|---|
| note | Mathlib proves `fib (n+1) / fib n → φ` as `n → ∞`. | Mathlib proves `fib (n+1) / fib n → Real.goldenRatio` as `n → ∞`. |
addedGamma function83c9e3a21305
addedLogistic map75d4250bcdee
addedIrrational numberd49ffe5caac7
addedTranscendental numberbdc59f7cee88