Commit 2026-03-21 18:59 1f7798f2

feat(Valued/ValuationTopology): Add and generalize lemmas for IsValuativeTopology (#36532) This is the first one of a series of PRs, with final goal removing the class Valued from Mathlib. A Valued instance will be replaced by [ValuativeRel R] [UniformSpace R] [IsValuativeTopogy R] [IsUniformAddGroup R] (v : Valuation R A) [v.Compatible]. If we have both [ValuativeRel R] and [TopologicalSpace R], then writing [IsValuativeTopology R] ensures that the topology on R agrees with the one induced by the valuation. The goal of this PR is to prepare (copy) all basic APIs of Valued in terms of IsValuativeTopology, mostly from the file Mathlib.Topology.Algebra.Valued.ValuationTopology to the new file Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology. The definition of IsValuativeTopology is also moved from Mathlib.RingTheory.Valuation.ValuativeRel.Basic into this new file. Currently in Mathlib, there already exists some lemmas with one variant stated with Valued and another variant stated with IsValuativeTopology. We make these APIs general enough to accept a valuation v with [v.Compatible] instead of just using ValuativeRel.valuation R. This PR would only prove these lemmas without actually replacing current existing Valued lemma.

More about the whole refactor plan:

1. Copy APIs that take Valued as input and make them accept input [ValuativeRel R] [UniformSpace R] [IsValuativeTopology R] [IsUniformAddGroup R] (v : Valuation R A) [v.Compatible]. (Starting with this PR.)
2. For every API that introduces a Valued instance, copy that API and make it create [ValuativeRel R] [UniformSpace R] [IsValuativeTopology R] [IsUniformAddGroup R] instances. And for every instance that currently exists in Mathlib, create the above series of instances as much as possible without introducing diamonds.
   More specifically, currently in Mathlib, there are three main ways of creating a Valued instance:
   • Valued.mk'
   • Valued.valuedCompletion
   • NormedField.toValued
     For each of these we create APIs to create the above series of instances.
3. A big PR deprecating the Valued class using 1 and 2.