Commit 2023-06-06 04:51 b8326f96

View on Github →

feat: port Analysis.SpecialFunctions.Exponential (#4713)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Exponential.lean

added theorem Complex.exp_eq_exp_ℂ

added theorem Real.exp_eq_exp_ℝ

added theorem hasDerivAt_exp

added theorem hasDerivAt_exp_of_mem_ball

added theorem hasDerivAt_exp_smul_const'

added theorem hasDerivAt_exp_smul_const

added theorem hasDerivAt_exp_smul_const_of_mem_ball'

added theorem hasDerivAt_exp_smul_const_of_mem_ball

added theorem hasDerivAt_exp_zero

added theorem hasDerivAt_exp_zero_of_radius_pos

added theorem hasFDerivAt_exp

added theorem hasFDerivAt_exp_of_mem_ball

added theorem hasFDerivAt_exp_smul_const'

added theorem hasFDerivAt_exp_smul_const

added theorem hasFDerivAt_exp_smul_const_of_mem_ball'

added theorem hasFDerivAt_exp_smul_const_of_mem_ball

added theorem hasFDerivAt_exp_zero

added theorem hasFDerivAt_exp_zero_of_radius_pos

added theorem hasStrictDerivAt_exp

added theorem hasStrictDerivAt_exp_of_mem_ball

added theorem hasStrictDerivAt_exp_smul_const'

added theorem hasStrictDerivAt_exp_smul_const

added theorem hasStrictDerivAt_exp_smul_const_of_mem_ball'

added theorem hasStrictDerivAt_exp_smul_const_of_mem_ball

added theorem hasStrictDerivAt_exp_zero

added theorem hasStrictDerivAt_exp_zero_of_radius_pos

added theorem hasStrictFDerivAt_exp

added theorem hasStrictFDerivAt_exp_of_mem_ball

added theorem hasStrictFDerivAt_exp_smul_const'

added theorem hasStrictFDerivAt_exp_smul_const

added theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball'

added theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball

added theorem hasStrictFDerivAt_exp_zero

added theorem hasStrictFDerivAt_exp_zero_of_radius_pos

Modified Mathlib/Data/Complex/Basic.lean