feat(Analysis.Normed.Ring.Seminorm): add SmoothingSeminorm

[mariainesdff]

We prove [BGR, Proposition 1.3.2/1][bosch-guntzer-remmert] : if f is a nonarchimedean seminorm on R, then iInf (λ (n : pnat), (f(x^(n : ℕ)))^(1/(n : ℝ))) is a power-multiplicative nonarchimedean seminorm on R.

---

• [ ] depends on: #18173
• [ ] depends on: #18172
• [ ] depends on: #18171
• [x] depends on: #16767
• [x] depends on: #16768
• [x] depends on: #16770