English
If c and d are differentiable at x and d(x) ≠ 0, then the derivative of c/d at x is (c'(x) d(x) − c(x) d'(x))/d(x)^2.
Русский
Если функции c и d дифференцируемы в точке x и d(x) ≠ 0, тогда производная дроби c/d в x равна (c'(x) d(x) − c(x) d'(x))/d(x)^2.
LaTeX
$$$ \\text{If } \\mathrm{d}c/dx, \\; \\mathrm{d}d/dx \\text{ exist at } x \\text{ 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_div (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) (hx : d x ≠ 0) :
deriv (c / d) x = (deriv c x * d x - c x * deriv d x) / d x ^ 2 :=
(hc.hasDerivAt.div hd.hasDerivAt hx).deriv
