English
If f is differentiable on s with continuous derivative, then c • f is differentiable on s for any scalar c from a semiring R with appropriate structure.
Русский
Если f дифференцируема на s, то константное умножение c · f дифференцируемо на s для любого скаляра c из поля/кольца, обладающего нужной структурой.
LaTeX
$$$\forall R\text{ with } \dots,\; \text{DiffContOnCl}(\mathit{f}, s) \Rightarrow \text{DiffContOnCl}(c \cdot \mathit{f}, s).$$$
Lean4
theorem const_smul {R : Type*} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F]
(hf : DiffContOnCl 𝕜 f s) (c : R) : DiffContOnCl 𝕜 (c • f) s :=
⟨hf.1.const_smul c, hf.2.const_smul c⟩