# mathlibdocumentation

topology.algebra.localization

# Localization of topological rings #

The topological localization of a topological commutative ring R at a submonoid M is the ring localization M endowed with the final ring topology of the natural homomorphism sending x : R to the equivalence class of (x, 1) in the localization of R at a M.

## Main Results #

• localization.topological_ring: The localization of a topological commutative ring at a submonoid is a topological ring.
def localization.ring_topology {R : Type u_1} [comm_ring R] {M : submonoid R} :

The ring topology on localization M coinduced from the natural homomorphism sending x : R to the equivalence class of (x, 1).

Equations
@[protected, instance]
def localization.topological_space {R : Type u_1} [comm_ring R] {M : submonoid R} :
Equations
@[protected, instance]
def localization.topological_ring {R : Type u_1} [comm_ring R] {M : submonoid R} :