Mathlib Map

Theorems · Theorem · functional analysis

hasStrictDerivAt_exp

∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {x : 𝕂}, HasStrictDerivAt NormedSpace.exp (NormedSpace.exp x) x

The exponential map in 𝕂 = ℝ or 𝕂 = ℂ has strict derivative NormedSpace.exp x at any point x.

Defined in
Mathlib.Analysis.SpecialFunctions.Exponential
Cited by
1 results in Mathlib
Foundations
Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
RCLike
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

hasDerivAt_exp · cited by 0hasDerivAt_expRCLike · cited by 2829RCLikeHasStrictDerivAt · cited by 163HasStrictDerivAtNormedSpace.exp · cited by 157NormedSpace.expedist_lt_top · cited by 32edist_lt_topNormedSpace.expSeries_radius_eq_top · cited by 27NormedSpace.expSeries_rad…hasStrictDerivAt_exp_of_mem_ball · cited by 2hasStrictDerivAt_exp_of_m…hasStrictDerivAt_expCITED BYCITES

Cites6

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

Cited by1

Results whose statement or proof uses this declaration.