English
Let c and d be differentiable functions; then the derivative of the function x ↦ c(x)/d(x) at x is (c'(x) d(x) − c(x) d'(x)) / d(x)^2, provided d(x) ≠ 0.
Русский
Пусть c и d дифференцируемы; производная функции x ↦ c(x)/d(x) в точке x равна (c'(x) d(x) − c(x) d'(x)) / d(x)^2 при d(x) ≠ 0.
LaTeX
$$$ \\text{If } c,d: \\mathbb{K} \\to \\mathbb{K}', \\; c',d' \\text{ exist, and } d(x) \\neq 0, \\; \\frac{d}{dx}\\left(\\frac{c(x)}{d(x)}\\right) = \\frac{c'(x) d(x) - c(x) d'(x)}{d(x)^2}. $$$
Lean4
@[simp]
theorem deriv_fun_div (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) (hx : d x ≠ 0) :
deriv (fun x => c x / d x) x = (deriv c x * d x - c x * deriv d x) / d x ^ 2 :=
(hc.hasDerivAt.div hd.hasDerivAt hx).deriv
