English
The operation of multiplying a C^n function by a constant is C^n in the target; same as contDiff_const_smul applied globally.
Русский
Операция умножения C^n-функции на константу сохраняет гладкость.
LaTeX
$$$\\\\forall c \\\\in R, \\\\ContDiff 𝕜 n f \\\\Rightarrow \\\\ContDiff 𝕜 n (\\\\lambda x. c \\\\cdot f(x))$$
Lean4
/-- The scalar multiplication of two `C^n` functions is `C^n`. -/
@[fun_prop]
theorem smul {f : E → 𝕜} {g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun x => f x • g x :=
contDiff_smul.comp (hf.prodMk hg)