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 (living in the same universe). Other instances are then deduced from