Properties_of_Exponential_Function
Provedanalysisexponentialproofwikireal-analysis
Properties of exp: exp(0) = 1, exp(x+y) = exp(x)*exp(y), and exp(x) > 0 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 Properties_of_Exponential_Function : Real.exp 0 = 1 ∧ ∀ x y : ℝ, Real.exp (x + y) = Real.exp x * Real.exp y ∧ 0 < Real.exp x := by sorry
Source