epi — Mathlib

English

Instance: Localization M induces an epimorphism in CommRingCat for the canonical map R → Localization M.

Русский

Инстанс: локализация M порождает эпиморфизм для канонического отображения R → Localization M.

LaTeX

$$$\mathrm{Localization}.epi\; M$$$

Lean4

instance epi {R : Type*} [CommRing R] (M : Submonoid R) : Epi (CommRingCat.ofHom <| algebraMap R <| Localization M) :=
  IsLocalization.epi M _

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