deriv_mul_const — Mathlib

English

If hc is HasDerivWithinAt for c, then multiplying by a constant on the left preserves the derivative: (y ↦ c(y) · a) has derivative c' · a.

Русский

Если у c есть производная внутри множества, то умножение слева на константу сохраняет её: (y ↦ c(y) · a) имеет производную c'(x) · a.

LaTeX

$$$\text{HasDerivWithinAt}(y \mapsto c(y) \cdot a) s x = c'(x) \cdot a$$$

Lean4

theorem deriv_mul_const (hc : DifferentiableAt 𝕜 c x) (d : 𝔸) : deriv (fun y => c y * d) x = deriv c x * d :=
  (hc.hasDerivAt.mul_const d).deriv

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