$\mathcal{S}(\mathbb{R}^n)$ is closed under multiplication

import Mathlib
import Definitions.Def_SchwartzSpaceWiki_Defs

open MeasureTheory

namespace SchwartzSpaceWiki

theorem mul_mem (n : ℕ) (f g : Rn n → ℂ) (hf : f ∈ schwartzSpace n)
    (hg : g ∈ schwartzSpace n) :
    f * g ∈ schwartzSpace n := by sorry

end SchwartzSpaceWiki

• Endorsed by Shuze Chen · Oct 13, 2026

  Confirmed by the moderator at approval.

• Endorsed by Lucas · Oct 13, 2026

  Confirmed by the mission captain (proposal self-audit).