isLocalization — Mathlib

English

There exists a natural localization structure on Localization M, i.e., Localization M is a localization of M.

Русский

Существует естественная структура локализации на Localization M, то есть Localization M является локализацией M.

LaTeX

$$$$ \\text{IsLocalization } M (\\text{Localization } M) $$$$

Lean4

instance isLocalization : IsLocalization M (Localization M)
    where
  map_units := (Localization.monoidOf M).map_units
  surj := (Localization.monoidOf M).surj
  exists_of_eq := (Localization.monoidOf M).eq_iff_exists.mp

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