# mathlib3documentation

analysis.calculus.deriv.linear

# Derivatives of continuous linear maps from the base field #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

@[protected]
theorem continuous_linear_map.has_deriv_at_filter {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {L : filter 𝕜} (e : 𝕜 →L[𝕜] F) :
(e 1) x L
@[protected]
theorem continuous_linear_map.has_strict_deriv_at {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} (e : 𝕜 →L[𝕜] F) :
(e 1) x
@[protected]
theorem continuous_linear_map.has_deriv_at {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} (e : 𝕜 →L[𝕜] F) :
(e 1) x
@[protected]
theorem continuous_linear_map.has_deriv_within_at {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {s : set 𝕜} (e : 𝕜 →L[𝕜] F) :
(e 1) s x
@[protected, simp]
theorem continuous_linear_map.deriv {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} (e : 𝕜 →L[𝕜] F) :
x = e 1
@[protected]
theorem continuous_linear_map.deriv_within {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {s : set 𝕜} (e : 𝕜 →L[𝕜] F) (hxs : x) :
x = e 1

### Derivative of bundled linear maps #

@[protected]
theorem linear_map.has_deriv_at_filter {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {L : filter 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
(e 1) x L
@[protected]
theorem linear_map.has_strict_deriv_at {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
(e 1) x
@[protected]
theorem linear_map.has_deriv_at {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
(e 1) x
@[protected]
theorem linear_map.has_deriv_within_at {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {s : set 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
(e 1) s x
@[protected, simp]
theorem linear_map.deriv {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F) :
x = e 1
@[protected]
theorem linear_map.deriv_within {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {s : set 𝕜} (e : 𝕜 →ₗ[𝕜] F) (hxs : x) :
x = e 1