toLocalizationMap — Mathlib

English

The construction toLocalizationMap is the localization map of R at M into S.

Русский

Построение toLocalizationMap является локализационной картой R по M в S.

LaTeX

$$toLocalizationMap : M.LocalizationMap S$$

Lean4

/-- `IsLocalization.toLocalizationMap M S` shows `S` is the monoid localization of `R` at `M`. -/
abbrev toLocalizationMap : M.LocalizationMap S
    where
  __ := algebraMap R S
  toFun := algebraMap R S
  map_units' := IsLocalization.map_units _
  surj' := IsLocalization.surj _
  exists_of_eq _ _ := IsLocalization.exists_of_eq

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