English
If c is strictly differentiable at x with derivative c', and u is a fixed finite-index family, then the map y ↦ (c(y)) u is strictly differentiable at x with derivative c'.flipMultilinear u.
Русский
Если c строго дифференцируема в x с производной c', а фиксировано задано множество индексов u, то f(y)=(c(y))u имеет строгую дифференцируемость в x с производной c'.flipMultilinear u.
LaTeX
$$$ HasStrictFDerivAt\left( y \mapsto (c(y)) u \right) x = c'.flipMultilinear(u)$$$
Lean4
theorem fderiv_continuousMultilinear_apply_const (hc : DifferentiableAt 𝕜 c x) (u : ∀ i, M i) :
(fderiv 𝕜 (fun y ↦ (c y) u) x) = (fderiv 𝕜 c x).flipMultilinear u :=
(hc.hasFDerivAt.continuousMultilinear_apply_const u).fderiv