María Inés de Frutos-Fernández

feat(topology/algebra/uniform_ring): ring completions and algebra structures

6

If `A` is an algebra over `R`, so is the `uniform_space.completion` of `A`. --- - [x] depends on: #14846 [](https://gitpod.io/from-referrer/)

feat(analysis/normed/ring_seminorm): add ring_seminorm, ring_norm

13

We define structures `ring_seminorm` and `ring_norm`. These definitions are useful when one needs to consider multiple (semi)norms on a given ring. --- [](https://gitpod.io/from-referrer/)

feat(ring_theory/dedekind_domain/finite_adele_ring): add finite_adele_ring

5

We define the finite adèle ring of a Dedekind domain and show that it is a commutative ring. --- [](https://gitpod.io/from-referrer/)

feat(analysis/normed/ring/seminorm_constructions): add seminorm_from_const

6

--- [](https://gitpod.io/from-referrer/)

feat(FieldTheory): add results about minpoly

1

--- [](https://gitpod.io/from-referrer/)

feat(Topology/Algebra/Algebra): add ContinuousAlgHom

1

We add the class `ContinuousAlgHom` for continuous algebra homomorphisms. Co-authored-by: Antoine Chambert-Loir --- [](https://gitpod.io/from-referrer/)

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

3

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...

feat(Order/Filer/ENNReal): add Real.limsup_mul_le

4

Lemmas about limsup and bddAbove needed for #15373. --- [](https://gitpod.io/from-referrer/)

feat(Algebra/Order/Field/Basic): add Nat cast lemmas

2

These lemmas have one-line proofs, but I use them enough times in #15373 that I think it makes sense to introduce them. --- [](https://gitpod.io/from-referrer/)