mathlib

1d4ed4a5 - chore(topology/algebra/valuation): use forgetful inheritance pattern for valued fields (#13691)

chore(topology/algebra/valuation): use forgetful inheritance pattern for valued fields (#13691) This allows us to solve a `uniform_space` diamond problem that arises when extending valuations to the completion of a valued field. More precisely, the main goal of this PR is to make the following work: ```lean import topology.algebra.valued_field example {K Γ₀ : Type*} [field K] [linear_ordered_comm_group_with_zero Γ₀] [valued K Γ₀] : uniform_space.completion.uniform_space K = valued.to_uniform_space := rfl ``` Co-authored-by: Patrick Massot <patrickmassot@free.fr>