# mathlib3documentation

analysis.calculus.fderiv.mul

# Multiplicative operations on derivatives #

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

For detailed documentation of the Fréchet derivative, see the module docstring of `analysis/calculus/fderiv/basic.lean`.

This file contains the usual formulas (and existence assertions) for the derivative of

• multiplication of a function by a scalar function
• multiplication of two scalar functions
• inverse function (assuming that it exists; the inverse function theorem is in `../inverse.lean`)

### Derivative of the pointwise composition/application of continuous linear maps #

theorem has_strict_fderiv_at.clm_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {x : E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {c' : E →L[𝕜] G →L[𝕜] H} {d : E (F →L[𝕜] G)} {d' : E →L[𝕜] F →L[𝕜] G} (hc : x) (hd : x) :
has_strict_fderiv_at (λ (y : E), (c y).comp (d y)) (( H) (c x)).comp d' + ( G H).flip) (d x)).comp c') x
theorem has_fderiv_within_at.clm_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {x : E} {s : set E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {c' : E →L[𝕜] G →L[𝕜] H} {d : E (F →L[𝕜] G)} {d' : E →L[𝕜] F →L[𝕜] G} (hc : s x) (hd : s x) :
has_fderiv_within_at (λ (y : E), (c y).comp (d y)) (( H) (c x)).comp d' + ( G H).flip) (d x)).comp c') s x
theorem has_fderiv_at.clm_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {x : E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {c' : E →L[𝕜] G →L[𝕜] H} {d : E (F →L[𝕜] G)} {d' : E →L[𝕜] F →L[𝕜] G} (hc : c' x) (hd : d' x) :
has_fderiv_at (λ (y : E), (c y).comp (d y)) (( H) (c x)).comp d' + ( G H).flip) (d x)).comp c') x
theorem differentiable_within_at.clm_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {x : E} {s : set E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {d : E (F →L[𝕜] G)} (hc : x) (hd : x) :
(λ (y : E), (c y).comp (d y)) s x
theorem differentiable_at.clm_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {x : E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {d : E (F →L[𝕜] G)} (hc : x) (hd : x) :
(λ (y : E), (c y).comp (d y)) x
theorem differentiable_on.clm_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {s : set E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {d : E (F →L[𝕜] G)} (hc : s) (hd : s) :
(λ (y : E), (c y).comp (d y)) s
theorem differentiable.clm_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {d : E (F →L[𝕜] G)} (hc : c) (hd : d) :
(λ (y : E), (c y).comp (d y))
theorem fderiv_within_clm_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {x : E} {s : set E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {d : E (F →L[𝕜] G)} (hxs : x) (hc : x) (hd : x) :
(λ (y : E), (c y).comp (d y)) s x = ( H) (c x)).comp d s x) + ( G H).flip) (d x)).comp c s x)
theorem fderiv_clm_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {x : E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {d : E (F →L[𝕜] G)} (hc : x) (hd : x) :
(λ (y : E), (c y).comp (d y)) x = ( H) (c x)).comp (fderiv 𝕜 d x) + ( G H).flip) (d x)).comp (fderiv 𝕜 c x)
theorem has_strict_fderiv_at.clm_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {G : Type u_4} [ G] {x : E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {c' : E →L[𝕜] G →L[𝕜] H} {u : E G} {u' : E →L[𝕜] G} (hc : x) (hu : x) :
has_strict_fderiv_at (λ (y : E), (c y) (u y)) ((c x).comp u' + (c'.flip) (u x)) x
theorem has_fderiv_within_at.clm_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {G : Type u_4} [ G] {x : E} {s : set E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {c' : E →L[𝕜] G →L[𝕜] H} {u : E G} {u' : E →L[𝕜] G} (hc : s x) (hu : s x) :
has_fderiv_within_at (λ (y : E), (c y) (u y)) ((c x).comp u' + (c'.flip) (u x)) s x
theorem has_fderiv_at.clm_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {G : Type u_4} [ G] {x : E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {c' : E →L[𝕜] G →L[𝕜] H} {u : E G} {u' : E →L[𝕜] G} (hc : c' x) (hu : u' x) :
has_fderiv_at (λ (y : E), (c y) (u y)) ((c x).comp u' + (c'.flip) (u x)) x
theorem differentiable_within_at.clm_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {G : Type u_4} [ G] {x : E} {s : set E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {u : E G} (hc : x) (hu : x) :
(λ (y : E), (c y) (u y)) s x
theorem differentiable_at.clm_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {G : Type u_4} [ G] {x : E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {u : E G} (hc : x) (hu : x) :
(λ (y : E), (c y) (u y)) x
theorem differentiable_on.clm_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {G : Type u_4} [ G] {s : set E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {u : E G} (hc : s) (hu : s) :
(λ (y : E), (c y) (u y)) s
theorem differentiable.clm_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {G : Type u_4} [ G] {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {u : E G} (hc : c) (hu : u) :
(λ (y : E), (c y) (u y))
theorem fderiv_within_clm_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {G : Type u_4} [ G] {x : E} {s : set E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {u : E G} (hxs : x) (hc : x) (hu : x) :
(λ (y : E), (c y) (u y)) s x = (c x).comp u s x) + c s x).flip) (u x)
theorem fderiv_clm_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {G : Type u_4} [ G] {x : E} {H : Type u_6} [ H] {c : E (G →L[𝕜] H)} {u : E G} (hc : x) (hu : x) :
(λ (y : E), (c y) (u y)) x = (c x).comp (fderiv 𝕜 u x) + ((fderiv 𝕜 c x).flip) (u x)

### Derivative of the product of a scalar-valued function and a vector-valued function #

If `c` is a differentiable scalar-valued function and `f` is a differentiable vector-valued function, then `λ x, c x • f x` is differentiable as well. Lemmas in this section works for function `c` taking values in the base field, as well as in a normed algebra over the base field: e.g., they work for `c : E → ℂ` and `f : E → F` provided that `F` is a complex normed vector space.

theorem has_strict_fderiv_at.smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} {c' : E →L[𝕜] 𝕜'} (hc : x) (hf : x) :
has_strict_fderiv_at (λ (y : E), c y f y) (c x f' + c'.smul_right (f x)) x
theorem has_fderiv_within_at.smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} {c' : E →L[𝕜] 𝕜'} (hc : s x) (hf : s x) :
has_fderiv_within_at (λ (y : E), c y f y) (c x f' + c'.smul_right (f x)) s x
theorem has_fderiv_at.smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} {c' : E →L[𝕜] 𝕜'} (hc : c' x) (hf : f' x) :
has_fderiv_at (λ (y : E), c y f y) (c x f' + c'.smul_right (f x)) x
theorem differentiable_within_at.smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hc : x) (hf : x) :
(λ (y : E), c y f y) s x
@[simp]
theorem differentiable_at.smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hc : x) (hf : x) :
(λ (y : E), c y f y) x
theorem differentiable_on.smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hc : s) (hf : s) :
(λ (y : E), c y f y) s
@[simp]
theorem differentiable.smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hc : c) (hf : f) :
(λ (y : E), c y f y)
theorem fderiv_within_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {s : set E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hxs : x) (hc : x) (hf : x) :
(λ (y : E), c y f y) s x = c x s x + c s x).smul_right (f x)
theorem fderiv_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {x : E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hc : x) (hf : x) :
(λ (y : E), c y f y) x = c x f x + (fderiv 𝕜 c x).smul_right (f x)
theorem has_strict_fderiv_at.smul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} {c' : E →L[𝕜] 𝕜'} (hc : x) (f : F) :
has_strict_fderiv_at (λ (y : E), c y f) (c'.smul_right f) x
theorem has_fderiv_within_at.smul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} {c' : E →L[𝕜] 𝕜'} (hc : s x) (f : F) :
has_fderiv_within_at (λ (y : E), c y f) (c'.smul_right f) s x
theorem has_fderiv_at.smul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} {c' : E →L[𝕜] 𝕜'} (hc : c' x) (f : F) :
has_fderiv_at (λ (y : E), c y f) (c'.smul_right f) x
theorem differentiable_within_at.smul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hc : x) (f : F) :
(λ (y : E), c y f) s x
theorem differentiable_at.smul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hc : x) (f : F) :
(λ (y : E), c y f) x
theorem differentiable_on.smul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {s : set E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hc : s) (f : F) :
(λ (y : E), c y f) s
theorem differentiable.smul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hc : c) (f : F) :
(λ (y : E), c y f)
theorem fderiv_within_smul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hxs : x) (hc : x) (f : F) :
(λ (y : E), c y f) s x = c s x).smul_right f
theorem fderiv_smul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {𝕜' : Type u_6} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} (hc : x) (f : F) :
(λ (y : E), c y f) x = (fderiv 𝕜 c x).smul_right f

### Derivative of the product of two functions #

theorem has_strict_fderiv_at.mul' {𝕜 : Type u_1} {E : Type u_2} [ E] {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a b : E 𝔸} {a' b' : E →L[𝕜] 𝔸} {x : E} (ha : x) (hb : x) :
has_strict_fderiv_at (λ (y : E), a y * b y) (a x b' + a'.smul_right (b x)) x
theorem has_strict_fderiv_at.mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸' : Type u_7} [normed_comm_ring 𝔸'] [ 𝔸'] {c d : E 𝔸'} {c' d' : E →L[𝕜] 𝔸'} (hc : x) (hd : x) :
has_strict_fderiv_at (λ (y : E), c y * d y) (c x d' + d x c') x
theorem has_fderiv_within_at.mul' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a b : E 𝔸} {a' b' : E →L[𝕜] 𝔸} (ha : s x) (hb : s x) :
has_fderiv_within_at (λ (y : E), a y * b y) (a x b' + a'.smul_right (b x)) s x
theorem has_fderiv_within_at.mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸' : Type u_7} [normed_comm_ring 𝔸'] [ 𝔸'] {c d : E 𝔸'} {c' d' : E →L[𝕜] 𝔸'} (hc : s x) (hd : s x) :
has_fderiv_within_at (λ (y : E), c y * d y) (c x d' + d x c') s x
theorem has_fderiv_at.mul' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a b : E 𝔸} {a' b' : E →L[𝕜] 𝔸} (ha : a' x) (hb : b' x) :
has_fderiv_at (λ (y : E), a y * b y) (a x b' + a'.smul_right (b x)) x
theorem has_fderiv_at.mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸' : Type u_7} [normed_comm_ring 𝔸'] [ 𝔸'] {c d : E 𝔸'} {c' d' : E →L[𝕜] 𝔸'} (hc : c' x) (hd : d' x) :
has_fderiv_at (λ (y : E), c y * d y) (c x d' + d x c') x
theorem differentiable_within_at.mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a b : E 𝔸} (ha : x) (hb : x) :
(λ (y : E), a y * b y) s x
@[simp]
theorem differentiable_at.mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a b : E 𝔸} (ha : x) (hb : x) :
(λ (y : E), a y * b y) x
theorem differentiable_on.mul {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a b : E 𝔸} (ha : s) (hb : s) :
(λ (y : E), a y * b y) s
@[simp]
theorem differentiable.mul {𝕜 : Type u_1} {E : Type u_2} [ E] {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a b : E 𝔸} (ha : a) (hb : b) :
(λ (y : E), a y * b y)
theorem differentiable_within_at.pow {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : x) (n : ) :
(λ (x : E), a x ^ n) s x
@[simp]
theorem differentiable_at.pow {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : x) (n : ) :
(λ (x : E), a x ^ n) x
theorem differentiable_on.pow {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : s) (n : ) :
(λ (x : E), a x ^ n) s
@[simp]
theorem differentiable.pow {𝕜 : Type u_1} {E : Type u_2} [ E] {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : a) (n : ) :
(λ (x : E), a x ^ n)
theorem fderiv_within_mul' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a b : E 𝔸} (hxs : x) (ha : x) (hb : x) :
(λ (y : E), a y * b y) s x = a x s x + a s x).smul_right (b x)
theorem fderiv_within_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸' : Type u_7} [normed_comm_ring 𝔸'] [ 𝔸'] {c d : E 𝔸'} (hxs : x) (hc : x) (hd : x) :
(λ (y : E), c y * d y) s x = c x s x + d x s x
theorem fderiv_mul' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a b : E 𝔸} (ha : x) (hb : x) :
(λ (y : E), a y * b y) x = a x b x + (fderiv 𝕜 a x).smul_right (b x)
theorem fderiv_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸' : Type u_7} [normed_comm_ring 𝔸'] [ 𝔸'] {c d : E 𝔸'} (hc : x) (hd : x) :
(λ (y : E), c y * d y) x = c x d x + d x c x
theorem has_strict_fderiv_at.mul_const' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} {a' : E →L[𝕜] 𝔸} (ha : x) (b : 𝔸) :
has_strict_fderiv_at (λ (y : E), a y * b) (a'.smul_right b) x
theorem has_strict_fderiv_at.mul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸' : Type u_7} [normed_comm_ring 𝔸'] [ 𝔸'] {c : E 𝔸'} {c' : E →L[𝕜] 𝔸'} (hc : x) (d : 𝔸') :
has_strict_fderiv_at (λ (y : E), c y * d) (d c') x
theorem has_fderiv_within_at.mul_const' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} {a' : E →L[𝕜] 𝔸} (ha : s x) (b : 𝔸) :
has_fderiv_within_at (λ (y : E), a y * b) (a'.smul_right b) s x
theorem has_fderiv_within_at.mul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸' : Type u_7} [normed_comm_ring 𝔸'] [ 𝔸'] {c : E 𝔸'} {c' : E →L[𝕜] 𝔸'} (hc : s x) (d : 𝔸') :
has_fderiv_within_at (λ (y : E), c y * d) (d c') s x
theorem has_fderiv_at.mul_const' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} {a' : E →L[𝕜] 𝔸} (ha : a' x) (b : 𝔸) :
has_fderiv_at (λ (y : E), a y * b) (a'.smul_right b) x
theorem has_fderiv_at.mul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸' : Type u_7} [normed_comm_ring 𝔸'] [ 𝔸'] {c : E 𝔸'} {c' : E →L[𝕜] 𝔸'} (hc : c' x) (d : 𝔸') :
has_fderiv_at (λ (y : E), c y * d) (d c') x
theorem differentiable_within_at.mul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : x) (b : 𝔸) :
(λ (y : E), a y * b) s x
theorem differentiable_at.mul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : x) (b : 𝔸) :
(λ (y : E), a y * b) x
theorem differentiable_on.mul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : s) (b : 𝔸) :
(λ (y : E), a y * b) s
theorem differentiable.mul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : a) (b : 𝔸) :
(λ (y : E), a y * b)
theorem fderiv_within_mul_const' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (hxs : x) (ha : x) (b : 𝔸) :
(λ (y : E), a y * b) s x = a s x).smul_right b
theorem fderiv_within_mul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸' : Type u_7} [normed_comm_ring 𝔸'] [ 𝔸'] {c : E 𝔸'} (hxs : x) (hc : x) (d : 𝔸') :
(λ (y : E), c y * d) s x = d s x
theorem fderiv_mul_const' {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : x) (b : 𝔸) :
(λ (y : E), a y * b) x = (fderiv 𝕜 a x).smul_right b
theorem fderiv_mul_const {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸' : Type u_7} [normed_comm_ring 𝔸'] [ 𝔸'] {c : E 𝔸'} (hc : x) (d : 𝔸') :
(λ (y : E), c y * d) x = d c x
theorem has_strict_fderiv_at.const_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} {a' : E →L[𝕜] 𝔸} (ha : x) (b : 𝔸) :
has_strict_fderiv_at (λ (y : E), b * a y) (b a') x
theorem has_fderiv_within_at.const_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} {a' : E →L[𝕜] 𝔸} (ha : s x) (b : 𝔸) :
has_fderiv_within_at (λ (y : E), b * a y) (b a') s x
theorem has_fderiv_at.const_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} {a' : E →L[𝕜] 𝔸} (ha : a' x) (b : 𝔸) :
has_fderiv_at (λ (y : E), b * a y) (b a') x
theorem differentiable_within_at.const_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : x) (b : 𝔸) :
(λ (y : E), b * a y) s x
theorem differentiable_at.const_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : x) (b : 𝔸) :
(λ (y : E), b * a y) x
theorem differentiable_on.const_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : s) (b : 𝔸) :
(λ (y : E), b * a y) s
theorem differentiable.const_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : a) (b : 𝔸) :
(λ (y : E), b * a y)
theorem fderiv_within_const_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (hxs : x) (ha : x) (b : 𝔸) :
(λ (y : E), b * a y) s x = b s x
theorem fderiv_const_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {𝔸 : Type u_6} [normed_ring 𝔸] [ 𝔸] {a : E 𝔸} (ha : x) (b : 𝔸) :
(λ (y : E), b * a y) x = b a x
theorem has_fderiv_at_ring_inverse {𝕜 : Type u_1} {R : Type u_6} [normed_ring R] [ R] (x : Rˣ) :

At an invertible element `x` of a normed algebra `R`, the Fréchet derivative of the inversion operation is the linear map `λ t, - x⁻¹ * t * x⁻¹`.

theorem differentiable_at_inverse {𝕜 : Type u_1} {R : Type u_6} [normed_ring R] [ R] {x : R} (hx : is_unit x) :
theorem differentiable_within_at_inverse {𝕜 : Type u_1} {R : Type u_6} [normed_ring R] [ R] {x : R} (hx : is_unit x) (s : set R) :
theorem differentiable_on_inverse {𝕜 : Type u_1} {R : Type u_6} [normed_ring R] [ R]  :
{x : R | is_unit x}
theorem fderiv_inverse {𝕜 : Type u_1} {R : Type u_6} [normed_ring R] [ R] (x : Rˣ) :
theorem differentiable_within_at.inverse {𝕜 : Type u_1} {E : Type u_2} [ E] {R : Type u_6} [normed_ring R] [ R] {h : E R} {z : E} {S : set E} (hf : z) (hz : is_unit (h z)) :
(λ (x : E), ring.inverse (h x)) S z
@[simp]
theorem differentiable_at.inverse {𝕜 : Type u_1} {E : Type u_2} [ E] {R : Type u_6} [normed_ring R] [ R] {h : E R} {z : E} (hf : z) (hz : is_unit (h z)) :
(λ (x : E), ring.inverse (h x)) z
theorem differentiable_on.inverse {𝕜 : Type u_1} {E : Type u_2} [ E] {R : Type u_6} [normed_ring R] [ R] {h : E R} {S : set E} (hf : S) (hz : (x : E), x S is_unit (h x)) :
(λ (x : E), ring.inverse (h x)) S
@[simp]
theorem differentiable.inverse {𝕜 : Type u_1} {E : Type u_2} [ E] {R : Type u_6} [normed_ring R] [ R] {h : E R} (hf : h) (hz : (x : E), is_unit (h x)) :
(λ (x : E), ring.inverse (h x))

### Derivative of the inverse in a division ring #

Note these lemmas are primed as they need `complete_space R`, whereas the other lemmas in `deriv/inv.lean` do not, but instead need `nontrivially_normed_field R`.

theorem has_fderiv_at_inv' {𝕜 : Type u_1} {R : Type u_6} [ R] {x : R} (hx : x 0) :
x

At an invertible element `x` of a normed division algebra `R`, the Fréchet derivative of the inversion operation is the linear map `λ t, - x⁻¹ * t * x⁻¹`.

theorem differentiable_at_inv' {𝕜 : Type u_1} {R : Type u_6} [ R] {x : R} (hx : x 0) :
theorem differentiable_within_at_inv' {𝕜 : Type u_1} {R : Type u_6} [ R] {x : R} (hx : x 0) (s : set R) :
(λ (x : R), x⁻¹) s x
theorem differentiable_on_inv' {𝕜 : Type u_1} {R : Type u_6} [ R]  :
(λ (x : R), x⁻¹) {x : R | x 0}
theorem fderiv_inv' {𝕜 : Type u_1} {R : Type u_6} [ R] {x : R} (hx : x 0) :

Non-commutative version of `fderiv_inv`

theorem fderiv_within_inv' {𝕜 : Type u_1} {R : Type u_6} [ R] {s : set R} {x : R} (hx : x 0) (hxs : x) :
(λ (x : R), x⁻¹) s x = - x⁻¹

Non-commutative version of `fderiv_within_inv`

theorem differentiable_within_at.inv' {𝕜 : Type u_1} {E : Type u_2} [ E] {R : Type u_6} [ R] {h : E R} {z : E} {S : set E} (hf : z) (hz : h z 0) :
(λ (x : E), (h x)⁻¹) S z
@[simp]
theorem differentiable_at.inv' {𝕜 : Type u_1} {E : Type u_2} [ E] {R : Type u_6} [ R] {h : E R} {z : E} (hf : z) (hz : h z 0) :
(λ (x : E), (h x)⁻¹) z
theorem differentiable_on.inv' {𝕜 : Type u_1} {E : Type u_2} [ E] {R : Type u_6} [ R] {h : E R} {S : set E} (hf : S) (hz : (x : E), x S h x 0) :
(λ (x : E), (h x)⁻¹) S
@[simp]
theorem differentiable.inv' {𝕜 : Type u_1} {E : Type u_2} [ E] {R : Type u_6} [ R] {h : E R} (hf : h) (hz : (x : E), h x 0) :
(λ (x : E), (h x)⁻¹)