Theorems · Definition · commutative algebra
Localization.ringTopology
{R : Type u_1} → [inst : CommRing R] → [TopologicalSpace R] → {M : Submonoid R} → RingTopology (Localization M)The ring topology on Localization M coinduced from the natural homomorphism sending x : R
to the equivalence class of (x, 1).
- Defined in
- Mathlib.Topology.Algebra.Localization
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingTopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- CommRingstatement and proof · cited by 17,173
- Submonoidstatement and proof · cited by 3,086
- Localizationstatement · cited by 270
- MulHom.toFunproof · cited by 36
- Localization.monoidOfproof · cited by 17
- RingTopologystatement · cited by 8
- Submonoid.LocalizationMap.toMulHomproof · cited by 2
- RingTopology.coinducedproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.