mathlib3

4c0aa6e7 - feat(analysis/schwartz): Definition of the Schwartz space (#15850)

feat(analysis/schwartz): Definition of the Schwartz space (#15850) This PR adds the definition of the Schwartz space and by abstract results also of tempered distributions. We prove basic algebraic and topological properties of the Schwartz space. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>