Theorems · Theorem · special functions

Complex.differentiable_exp

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ], Differentiable 𝕜 Complex.exp

Defined in: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Cited by: 4 results in Mathlib
Foundations: Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NontriviallyNormedField NormedAlgebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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

NontriviallyNormedFieldstatement and proof · cited by 8,742
Complexstatement and proof · cited by 5,565
NormedAlgebrastatement and proof · cited by 1,165
Complex.expstatement · cited by 612
Differentiablestatement · cited by 298
HasDerivAt.differentiableAtproof · cited by 73
Complex.hasDerivAt_expproof · cited by 10
DifferentiableAt.restrictScalarsproof · cited by 6

Cited by4

Results whose statement or proof uses this declaration.

PhragmenLindelof.quadrant_Iproof · cited by 4
Complex.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countableproof · cited by 2
PhragmenLindelof.eq_zero_on_right_half_plane_of_superexponential_decayproof · cited by 1
Complex.differentiableAt_expproof · cited by 0