deriv_div_const

Mathlib.Analysis.Calculus.Deriv.Mul

URI: https://scilib.ai/kg/mathlib#deriv_div_const

English

Same as above: the derivative of c(x)/d is (deriv c(x))/d.

Русский

То же самое: производная c(x)/d равна deriv c(x) делённому на d.

LaTeX

$$$\\text{deriv}(c(x)/d) = (\\text{deriv } c(x))/d$$$

Lean4

@[simp]
theorem deriv_div_const (d : 𝕜') : deriv (fun x => c x / d) x = deriv c x / d := by
  simp only [div_eq_mul_inv, deriv_mul_const_field]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru