# Derivatives of continuous linear maps from the base field #

In this file we prove that f : 𝕜 →L[𝕜] E (or f : 𝕜 →ₗ[𝕜] E) has derivative f 1.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of Analysis/Calculus/Deriv/Basic.

## Keywords #

derivative, linear map

### Derivative of continuous linear maps #

theorem ContinuousLinearMap.hasDerivAtFilter {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {L : } (e : 𝕜 →L[𝕜] F) :
HasDerivAtFilter (e) (e 1) x L
theorem ContinuousLinearMap.hasStrictDerivAt {𝕜 : Type u} {F : Type v} [] {x : 𝕜} (e : 𝕜 →L[𝕜] F) :
HasStrictDerivAt (e) (e 1) x
theorem ContinuousLinearMap.hasDerivAt {𝕜 : Type u} {F : Type v} [] {x : 𝕜} (e : 𝕜 →L[𝕜] F) :
HasDerivAt (e) (e 1) x
theorem ContinuousLinearMap.hasDerivWithinAt {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →L[𝕜] F) :
HasDerivWithinAt (e) (e 1) s x
@[simp]
theorem ContinuousLinearMap.deriv {𝕜 : Type u} {F : Type v} [] {x : 𝕜} (e : 𝕜 →L[𝕜] F) :
deriv (e) x = e 1
theorem ContinuousLinearMap.derivWithin {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →L[𝕜] F) (hxs : ) :
derivWithin (e) s x = e 1

### Derivative of bundled linear maps #

theorem LinearMap.hasDerivAtFilter {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {L : } (e : 𝕜 →ₗ[𝕜] F) :
HasDerivAtFilter (e) (e 1) x L
theorem LinearMap.hasStrictDerivAt {𝕜 : Type u} {F : Type v} [] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
HasStrictDerivAt (e) (e 1) x
theorem LinearMap.hasDerivAt {𝕜 : Type u} {F : Type v} [] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
HasDerivAt (e) (e 1) x
theorem LinearMap.hasDerivWithinAt {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
HasDerivWithinAt (e) (e 1) s x
@[simp]
theorem LinearMap.deriv {𝕜 : Type u} {F : Type v} [] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
deriv (e) x = e 1
theorem LinearMap.derivWithin {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →ₗ[𝕜] F) (hxs : ) :
derivWithin (e) s x = e 1