Moritz Doll

We should have almost everything to prove the general Banach-Alaoglu theorem. One reference would be Chapter 8 in the book by Narici-Beckenstein. The main ingredients still missing are the completeness...

We have the definition of locally convex spaces and the characterization of locally convex spaces via seminorms. We have all the ingredients to prove the very useful lemma: Let X...

Right now `to_ring_hom_eq_coe` is not a simp lemma, which makes it not possible to deduce something like `(f : R ≃+* S) : ⇑(f.to_ring_hom) = ⇑f` by `simp`. The open...

feat(Analysis/TemperedDistribution): multiplication with temperate growth functions

3

The multiplication with a temperate growth function as a continuous linear map on tempered distributions. --- [](https://gitpod.io/from-referrer/)