Theorems · Theorem · real analysis

HasDerivAt.cpow

∀ {f g : ℂ → ℂ} {f' g' x : ℂ},
  HasDerivAt f f' x →
    HasDerivAt g g' x →
      f x ∈ Complex.slitPlane →
        HasDerivAt (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 213 from the axioms · uses propext, Classical.choice, Quot.sound