# mathlibdocumentation

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ˣ) :
theorem fderiv_inverse {𝕜 : Type u_1} {R : Type u_6} [normed_ring R] [ R] (x : Rˣ) :