topology on a valued ring

Stream: condensed mathematics

[Kevin Buzzard]

There is a bunch of stuff in the perfectoid project which needs to be ported to mathlib -- this is true independent of the challenge. Patrick and I are currently working on porting some stuff about the topology on a ring induced by a valuation. One should really do this properly so the proposal is to port a whole bunch of perfectoid stuff about topologies on groups induced by filter bases at 1 which play well with respect to the group structure.