div_const — Mathlib

English

If c has derivative c' at x, then the derivative of y ↦ c(y) / d is c'(x) / d for any constant d.

Русский

Если c имеет производную c'(x) в x, то производная от y ↦ c(y) / d равна c'(x) / d для любой константы d.

LaTeX

$$$ \text{HasDerivAt}(c, c', x) \Rightarrow \frac{d}{dx} \left( \frac{c(x)}{d} \right) = \frac{c'(x)}{d} $$$

Lean4

theorem div_const (hc : HasDerivAt c c' x) (d : 𝕜') : HasDerivAt (fun x => c x / d) (c' / d) x := by
  simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹

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