ringTopology — Mathlib

English

The ring topology on Localization M is defined as the coinduced topology along the natural map sending x to the class of (x,1).

Русский

Топология кольца на локализации Localization M задаётся как когинерализованная топология по естественному отображению x ↦ класс (x,1).

LaTeX

$$$\\text{ringTopology} : RingTopology(Localization M) = \\\\ RingTopology.coinduced( Localization.monoidOf M).toFun$$$

Lean4

/-- The ring topology on `Localization M` coinduced from the natural homomorphism sending `x : R`
to the equivalence class of `(x, 1)`. -/
def ringTopology : RingTopology (Localization M) :=
  RingTopology.coinduced (Localization.monoidOf M).toFun

Похожие утверждения