feat: port Analysis.SchwartzSpace (#4762)

Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
leanprover-community · Jun 19, 2023 · c10de4a · c10de4a
1 parent 10d3348
commit c10de4a
Show file tree

Hide file tree

Showing 2 changed files with 1,048 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -691,6 +691,7 @@ import Mathlib.Analysis.ODE.Gronwall
 import Mathlib.Analysis.ODE.PicardLindelof
 import Mathlib.Analysis.PSeries
 import Mathlib.Analysis.Quaternion
+import Mathlib.Analysis.SchwartzSpace
 import Mathlib.Analysis.Seminorm
 import Mathlib.Analysis.SpecialFunctions.Arsinh
 import Mathlib.Analysis.SpecialFunctions.Bernstein