Theorems · Definition · group theory

AddLocalization.addEquivOfQuotient

{M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} → {N : Type u_2} → [inst_1 : AddCommMonoid N] → S.LocalizationMap N → AddLocalization S ≃+ N

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.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Maps

Cited by

7 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidAddCommMonoid