Commit 2026-09-25 16:01 e8a0dfd3
View on Github →feat(Valued/ValuationTopology): creating instances of IsValuativeTopology on completion (#36769)
Main description
In this PR, we extend ValuativeRel to the completion of a topological field K and show the extension is compatible with the topology if the original relation is compatible with the topology on K.
Entry point for reviewing
In file Mathlib/Topology/Algebra/ValuativeRel/Completion.lean, we define Valuation.extension (resp. UniformSpace.Completion.valuativeRel) that extends a valuation (resp. a valuative relation) on a field K to Completion K.