Theorems · Theorem · real analysis

HasStrictDerivAt.cpow

∀ {f g : ℂ → ℂ} {f' g' x : ℂ},
  HasStrictDerivAt f f' x →
    HasStrictDerivAt g g' x →
      f x ∈ Complex.slitPlane →
        HasStrictDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x

Defined in

Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Cited by

1 results in Mathlib

Foundations

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