fderiv_eq_deriv_mul — Mathlib

English

For a real-valued function f: 𝕜 → 𝕜, the derivative of f at x, as a linear map, acts by multiplication by deriv f x; equivalently, (fderiv 𝕜 f x : 𝕜 → 𝕜) y = (deriv f x) · y.

Русский

Для f: 𝕜 → 𝕜 производная как линейное отображение умножает вход на производную в x: (fderiv 𝕜 f x)(y) = (deriv f x) • y.

LaTeX

$$$$ (fderiv 𝕜 f x : 𝕜 \\to 𝕜) y = (\\\\ deriv f x) \\\\cdot y $$$$

Lean4

theorem fderiv_eq_deriv_mul {f : 𝕜 → 𝕜} {x y : 𝕜} : (fderiv 𝕜 f x : 𝕜 → 𝕜) y = (deriv f x) * y := by simp [mul_comm]

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