Some results on metric completions I don't find

Stream: Is there code for X?

[Claudio Sacerdoti Coen]

CauSeq.Completion.Cauchy allows to complete a field w.r.t. an absolute value abs.
I don't manage to find the following results: are they trivial consequences of something already in Mathlib?

1. the completion is a completion of valued fields, i.e. it induces an absolute value on the target of the completion defined as the limit of the cauchy sequences/filters of absolute values. The result is there only for complex numbers, but it does not use a general construction
2. completing w.r.t. equivalent absolute values yields equivalent absolute values
3. 1+2: the induced absolute values are equivalent when the completion starts from equivalent absolute values

Just to give the context, these are lemmas used in the generalization of Ostrowki theorem to number fields (currently missing in Mathlib) that I am tackling as an exercise.

[Michael Stoll]

docs#AbsoluteValue.Completion ?

[María Inés de Frutos Fernández]

@Fabrizio Barroero, are you still working on Ostrowski for number fields?

[Fabrizio Barroero]

The nonarchimedean case only misses a fact about localizations which would be good to prove in higher generality.
I plan to work on that but I am very busy because the semester is starting…