Diff — Euler's formula

Revision #2987 → #3477 · back to history

modifiede is the base of the natural logarithm9a9687e72a44

Field	From #2987	To #3477
note	Mathlib's `Real.log` is defined as the inverse of `Real.exp`; `Real.log_exp x : Real.log (Real.exp x) = x` witnesses e = exp 1 as the base (the previously cited `Real.exp_one_eq_exp` does not exist).	Mathlib's `Real.log` is defined as the inverse of `Real.exp`; `Real.log_exp x : Real.log (Real.exp x) = x` witnesses e = exp 1 as the base.

addedCosine and sine of a real number as real and imaginary parts of e^{ix}ee570d9bc763

addedComplex cosine plus i sine equals exp(x*I)9e2a6e5c45cd

addedModulus of a complex number4fc7612eec24

addedComplex conjugate0d4f2ca5c634

addedLogarithm of a product05acad1938ad