English
If f has derivative f' at x and h is differentiable at x, then the derivative of f ∘ h at x is h' · f'(h x).
Русский
Если f дифференцируема в x с производной f', а h дифференцируема в x с производной h', то производная композиции f ∘ h в x равна h' · f'(h x).
LaTeX
$$$\text{If } f \text{ is differentiable at } x \text{ with derivative } f' \text{ and } h \text{ is differentiable at } x \text{ with derivative } h', \text{ then } (f \circ h)'(x) = h' \cdot f'(h x).$$$
Lean4
/-- If `f` is differentiable at `x`, and `L` is `σ`-semilinear, then `L ∘ f ∘ σ⁻¹` is
differentiable at `σ x`. -/
theorem comp_ringHom (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (σ ∘ f ∘ σ') (σ x) :=
(hf.hasDerivAt.comp_ringHom σ σ').differentiableAt
