Theorems · Theorem · special functions

HasStrictDerivAt.cexp

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {f : 𝕜 → ℂ} {f' : ℂ} {x : 𝕜},
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Complex.exp (f x)) (Complex.exp (f x) * f') x

Defined in

Mathlib.Analysis.SpecialFunctions.ExpDeriv

Cited by

6 results in Mathlib

Foundations

Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAlgebra