fderiv_mul_const' — Mathlib

English

If a is differentiable at x with derivative a', then the derivative of y ↦ a(y) is a' multiplied by the constant.

Русский

Если a дифференцируема в x с производной a', то производная y ↦ a(y) умножено на константу равна a' применяемая к этой константе.

LaTeX

$$$\\forall ha, b,\\ fderiv 𝕜 (y \\mapsto a(y) b) x = a' \\cdot b$$$

Lean4

theorem fderiv_mul_const' (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) : fderiv 𝕜 (fun y => a y * b) x = fderiv 𝕜 a x <• b :=
  (ha.hasFDerivAt.mul_const' b).fderiv

Похожие утверждения