Theorems · Definition · commutative algebra

ValuativeRel.uniformSpace

(R : Type u_1) → [inst : Ring R] → [ValuativeRel R] → UniformSpace R

The uniform structure induced by a valuative relation. Note that this is not made into a global instance to avoid diamonds. If desired, one can equip a ring with a uniform space from a valuative relation by hand. But as long as they do so, the fact that the topology is valuative and nonarchimedean, and the addition is uniformly continuous, can be automatically inferred.

Defined in

Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Cited by

1 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingValuativeRel