feat(topology/algebra): nonarchimedean filter bases (#9511)
feat(topology/algebra): nonarchimedean filter bases (#9511)

This is preparatory material for adic topology. It is a modernized version of code from the perfectoid spaces project.





leanprover-community/mathlib,leanprover-community/mathlib