mulEquivOfQuotient — Mathlib

English

Localization quotient isomorphism between monoid of S and the localization at S.

Русский

Изоморфизм отношения локализации между моноидом S и локализацией S.

LaTeX

$$$Localization.mulEquivOfQuotient f = (Localization.monoidOf S).mulEquivOfLocalizations f$$$

Lean4

/-- Given a Localization map `f : M →* N` for a Submonoid `S`, we get an isomorphism between
the Localization of `M` at `S` as a quotient type and `N`. -/
@[to_additive /-- Given a Localization map `f : M →+ N` for a Submonoid `S`, we get an isomorphism between
    the Localization of `M` at `S` as a quotient type and `N`. -/
    ]
noncomputable def mulEquivOfQuotient (f : Submonoid.LocalizationMap S N) : Localization S ≃* N :=
  (monoidOf S).mulEquivOfLocalizations f

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