mul_const — Mathlib

English

If hc is HasDerivAt for c with derivative c' and d is a constant, then (y ↦ c(y) · d) has derivative c' · d at x.

Русский

Если у c есть производная в x, и d константа, то производная от y ↦ c(y) · d равна c'(x) · d.

LaTeX

$$$\text{HasDerivAt}(y \mapsto c(y) \cdot d) x = c'(x) \cdot d$$$

Lean4

theorem mul_const (hc : HasStrictDerivAt c c' x) (d : 𝔸) : HasStrictDerivAt (fun y => c y * d) (c' * d) x :=
  by
  convert hc.mul (hasStrictDerivAt_const x d) using 1
  rw [mul_zero, add_zero]

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