English
Derivative of star(f) equals starL' composed with derivative of f.
Русский
Производная от star(f) равна композиции starL' с производной f.
LaTeX
$$$\\text{fderiv}_{\\mathbb{K}}(\\mathrm{star}(f))\\; x = (\\mathrm{starL'}_{\\mathbb{K}}) \\circ_L \\text{fderiv}_{\\mathbb{K}}(f)\\; x$$$
Lean4
@[simp]
theorem fderiv_star : fderiv 𝕜 (fun y => star (f y)) x = ((starL' 𝕜 : F ≃L[𝕜] F) : F →L[𝕜] F) ∘L fderiv 𝕜 f x :=
(starL' 𝕜 : F ≃L[𝕜] F).comp_fderiv