Theorems · Theorem · real analysis

Complex.derivWithin_const_cpow

∀ {f : ℂ → ℂ} {s : Set ℂ} {x : ℂ},
  DifferentiableWithinAt ℂ f s x →
    ∀ (c : ℂ), derivWithin (fun x => c ^ f x) s x = Complex.log c * derivWithin f s x * c ^ f x

Defined in: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Cited by: 1 results in Mathlib
Foundations: Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Complexstatement and proof · cited by 5,565
mul_commproof · cited by 2,262
MulZeroClass.mul_zeroproof · cited by 2,091
nhdsWithinproof · cited by 1,912
mul_assocproof · cited by 1,667
MulZeroClass.zero_mulproof · cited by 1,625
DifferentiableWithinAtstatement and proof · cited by 453
Filter.Frequentlyproof · cited by 414
derivWithinstatement and proof · cited by 258
UniqueDiffWithinAtproof · cited by 252
Complex.logstatement and proof · cited by 187

Cited by1

Results whose statement or proof uses this declaration.

Complex.deriv_const_cpowproof · cited by 0