Theorems · Theorem · real analysis

HasDerivWithinAt.cpow

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

Defined in

Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Cited by

0 results in Mathlib

Foundations

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