smul_const — Mathlib

English

If c has derivative c' at x, then y ↦ c(y) · f has derivative c'.smulRight f at x.

Русский

Если у c в x существует производная c', то функция y ↦ c(y) · f имеет производную в x равную c'.smulRight f.

LaTeX

$$$\HasFDerivAt\ c\ c'\ x \Rightarrow \HasFDerivAt\ (\\lambda y. c(y) \\cdot f)\ (c'.smulRight f)\ x$$$

Lean4

@[fun_prop]
theorem smul_const (hc : HasFDerivAt c c' x) (f : F) : HasFDerivAt (fun y => c y • f) (c'.smulRight f) x := by
  simpa only [smul_zero, zero_add] using hc.smul (hasFDerivAt_const f x)

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