The topology on a valued ring #
In this file, we define the non archimedean topology induced by a valuation on a ring.
The main definition is a
Valued type class which equips a ring with a valuation taking
values in a group with zero. Other instances are then deduced from this.
- isOpen_univ : TopologicalSpace.IsOpen Set.univ
- symm : Filter.Tendsto Prod.swap s.uniformity s.uniformity
- v : Valuation R Γ₀
A valued ring is a ring that comes equipped with a distinguished valuation. The class
is designed for the situation that there is a canonical valuation on the ring.
TODO: show that there always exists an equivalent valuation taking values in a type belonging to the same universe as the ring.