Commit 2022-04-29 20:31 1d4ed4a5

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:

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