instZSMul — Mathlib

English

There is an integer action on Schwartz maps: for each integer n, n • f is defined as the integer-scalar multiplication.

Русский

Действие целых чисел на SchwartzMap: для каждого целого n определяется n • f.

LaTeX

$$$ (n \\cdot f)(x) = n \\cdot f(x) $$$

Lean4

instance instZSMul : SMul ℤ 𝓢(E, F) :=
  ⟨fun c f =>
    { toFun := c • (f : E → F)
      smooth' := (f.smooth _).const_smul c
      decay' := by simpa [← Int.cast_smul_eq_zsmul ℝ] using ((c : ℝ) • f).decay' }⟩

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