English
If c and d are differentiable within the whole domain, and d never vanishes, then (the derivative of c/d) at x is (dc(x) d(x) − c(x) dd(x)) / d(x)^2.
Русский
Если c и d дифференцируемы во всём домене, и d(x) ≠ 0, то производная функции x ↦ c(x)/d(x) в точке x равна (c'(x) d(x) − c(x) d'(x))/d(x)^2.
LaTeX
$$$ \\text{If } Dc\\text{ and } Dd\\text{ exist, and } d(x) \\neq 0, \\; \\frac{d}{dx}(c/d) = \\frac{c'(x) d(x) - c(x) d'(x)}{d(x)^2}. $$$
Lean4
theorem derivWithin_div (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) (hx : d x ≠ 0) :
derivWithin (c / d) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2 :=
derivWithin_fun_div hc hd hx
