div — Mathlib

English

If hc and hd are HasDerivAt c c' x and HasDerivAt d d' x with d x ≠ 0, then HasDerivAt (c/d) with derivative (c' d x - c x d')/d x^2 at x.

Русский

Если имеют место HasDerivAt для c и d в точке x, и d(x) ≠ 0, то производная c/d существует и равна (c' d x − c x d')/d x^2 в точке x.

LaTeX

$$$\\forall {hc hd hx}, HasDerivAt (c/d) ( (c' d x - c x d')/d x^2 ) x$$$

Lean4

theorem div (hc : HasDerivAt c c' x) (hd : HasDerivAt d d' x) (hx : d x ≠ 0) :
    HasDerivAt (c / d) ((c' * d x - c x * d') / d x ^ 2) x :=
  hc.fun_div hd hx

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