Documentation

Mathlib.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 an M.

Main Results #

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

Equations
Instances For
    Equations
    • instTopologicalSpaceLocalization = Localization.ringTopology.toTopologicalSpace