# Documentation

Mathlib.Analysis.Calculus.Deriv.Star

# Star operations on derivatives #

This file contains the usual formulas (and existence assertions) for the derivative of the star operation. Note that these only apply when the field that the derivative is respect to has a trivial star operation; which as should be expected rules out 𝕜 = ℂ.

### Derivative of x ↦ star x#

theorem HasDerivAtFilter.star {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} [] [] [] [] [] {f' : F} {x : 𝕜} {L : } (h : HasDerivAtFilter f f' x L) :
HasDerivAtFilter (fun x => star (f x)) (star f') x L
theorem HasDerivWithinAt.star {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} [] [] [] [] [] {f' : F} {s : Set 𝕜} {x : 𝕜} (h : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun x => star (f x)) (star f') s x
theorem HasDerivAt.star {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} [] [] [] [] [] {f' : F} {x : 𝕜} (h : HasDerivAt f f' x) :
HasDerivAt (fun x => star (f x)) (star f') x
theorem HasStrictDerivAt.star {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} [] [] [] [] [] {f' : F} {x : 𝕜} (h : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun x => star (f x)) (star f') x
theorem derivWithin.star {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} [] [] [] [] [] {s : Set 𝕜} {x : 𝕜} (hxs : ) :
derivWithin (fun y => star (f y)) s x = star (derivWithin f s x)
theorem deriv.star {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} [] [] [] [] [] {x : 𝕜} :
deriv (fun y => star (f y)) x = star (deriv f x)
@[simp]
theorem deriv.star' {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} [] [] [] [] [] :
(deriv fun y => star (f y)) = fun x => star (deriv f x)