Mathlib Map

Theorems · Theorem · special functions

Complex.hasStrictDerivAt_exp

∀ (x : ℂ), HasStrictDerivAt Complex.exp (Complex.exp x) x
Defined in
Mathlib.Analysis.SpecialFunctions.ExpDeriv
Cited by
8 results in Mathlib
Foundations
Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Complex.hasStrictDerivAt_log · cited by 8Complex.hasStrictDerivAt_…HasStrictDerivAt.cexp · cited by 6HasStrictDerivAt.cexpComplex.hasStrictDerivAt_cosh · cited by 4Complex.hasStrictDerivAt_…Complex.hasStrictDerivAt_sinh · cited by 4Complex.hasStrictDerivAt_…Real.hasStrictDerivAt_exp · cited by 3Real.hasStrictDerivAt_expHasStrictFDerivAt.cexp · cited by 1HasStrictFDerivAt.cexpComplex.isOpenMap_exp · cited by 1Complex.isOpenMap_expComplex.hasStrictFDerivAt_exp_real · cited by 0Complex.hasStrictFDerivAt…Complex · cited by 5565Complexone_ne_zero · cited by 885one_ne_zeroComplex.exp · cited by 612Complex.expHasStrictDerivAt · cited by 163HasStrictDerivAtContDiff.contDiffAt · cited by 106ContDiff.contDiffAtComplex.contDiff_exp · cited by 11Complex.contDiff_expComplex.hasDerivAt_exp · cited by 10Complex.hasDerivAt_expContDiffAt.hasStrictDerivAt' · cited by 2ContDiffAt.hasStrictDeriv…Complex.hasStrictDerivAt_expCITED BYCITES

Cites8

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

Cited by8

Results whose statement or proof uses this declaration.