Power_Series_Expansion_for_Exponential
Provedanalysisexponentialpower-seriesproofwiki
exp(x) = sum_{n=0}^{infinity} x^n / n! for all real x.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.SpecialFunctions.ExpDeriv
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.SpecialFunctions.ExpDeriv theorem Power_Series_Expansion_for_Exponential (x : ℝ) : HasSum (fun n => x ^ n / Nat.factorial n) (Real.exp x) := by sorry
Source