fderiv_const_smul_of_invertible — Mathlib

English

In the invertible scalar setting, DifferentiableWithinAt (c · f) s x is equivalent to DifferentiableWithinAt f s x.

Русский

В условиях обратимого скаляра, DifferentiableWithinAt (c · f) s x эквивалентно DifferentiableWithinAt f s x.

LaTeX

$$$ \text{DifferentiableWithinAt}_{\mathbb{K}} (c \cdot f) \, s \, x \iff \text{DifferentiableWithinAt}_{\mathbb{K}} f \, s \, x$$$

Lean4

/-- A version of `fderiv_const_smul` without differentiability hypothesis: in return, the constant
`c` must be invertible, i.e. if `R` is a field. -/
theorem fderiv_const_smul_of_invertible (c : R) [Invertible c] : fderiv 𝕜 (c • f) x = c • fderiv 𝕜 f x := by
  simp [← fderivWithin_univ, fderivWithin_const_smul_of_invertible c uniqueDiffWithinAt_univ]

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