deriv_comp_mul_left — Mathlib

English

The derivative within s of f(c x) equals c times the derivative within c·s of f at c x.

Русский

Производная внутри s от f(c x) равна c умноженному на производную внутри c·s от f в точке c x.

LaTeX

$$$$derivWithin\ (fun x => f(\,c * x\,))\ s x = c \cdot derivWithin\ f (c \cdot s) (c \cdot x)$$$$

Lean4

theorem deriv_comp_mul_left : deriv (f <| c * ·) x = c • deriv f (c * x) := by
  simp only [← smul_eq_mul, deriv, fderiv_comp_smul, ContinuousLinearMap.smul_apply]

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