mathlib3

510e65d7 - feat(topology/algebra/localization): add topological localization (#8894)

feat(topology/algebra/localization): add topological localization (#8894) We show that ring topologies on a ring `R` form a complete lattice. We use this to define the topological localization of a topological commutative ring `R` at a submonoid `M`. Co-authored-by: Johan Commelin <johan@commelin.net>