Revision #1176 → #1816 · back to history
modifiedDerivative of general exponential0774a91042b8
| Field | From #1176 | To #1816 |
|---|
| mathlib.decl | Real.hasDerivAt_const_rpow | Real.hasStrictDerivAt_const_rpow |
| note | Mathlib has the derivative of `a^x` via rpow (giving `a^x * log a`) though it is computed without going through the limit definition. | Mathlib gives the derivative of `a^x` via rpow as `a^x * log a`, computed without going through the limit definition. |
modifiede is transcendental (Hermite)b9492ad4203e
| Field | From #1176 | To #1816 |
|---|
| mathlib.decl | LindemannWeierstrass | LindemannWeierstrass.exp_polynomial_approx |
modifiedSeries for computing e656e94d7d733
| Field | From #1176 | To #1816 |
|---|
| mathlib.decl | NormedSpace.exp_eq_tsum_div | Real.exp_one_near_20 |
| mathlib.module | Mathlib.Analysis.Normed.Algebra.Exponential | Mathlib.Analysis.Complex.ExponentialBounds |
addede is irrational (lead)e57d25a9ceae
addede is transcendental (lead)50815191bea9
addedEuler's identity (lead)b8848ad890fa
addedEquivalence of limit and series definitionse90ea08a2681
addedExponential identity for derivativeea2c9ef39f3d
addedNatural logarithm as inverse of expd9d3d30cfa75
addedBernoulli's inequality limiting case735c3708ba99
addedCosine and sine via exponential8caa4cac0360
addedAlgebraic independence of e and π33ab0a0f2975
addede is normal58581373c2c3