fderiv_const_smul_of_field — Mathlib

English

If c is invertible, then fderivWithin (c · f) at x equals c times fderivWithin f at x.

Русский

Если c обратим, то fderivWithin (c · f) в x равен c · fderivWithin f в x.

LaTeX

$$$ fderivWithin 𝕜 (c \cdot f) \, s \, x = c \, fderivWithin 𝕜 f \, s \, x$$$

Lean4

/-- Special case of `fderiv_const_smul_of_invertible` over a field: any constant is allowed -/
theorem fderiv_const_smul_of_field (c : 𝕜) : fderiv 𝕜 (c • f) = c • fderiv 𝕜 f :=
  by
  simp_rw [← fderivWithin_univ]
  ext x
  simp [fderivWithin_const_smul_of_field c uniqueDiffWithinAt_univ]

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