Theorems · Definition · group theory

AddMonoidHom.toLocalizationMap

{M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {N : Type u_2} →
        [inst_1 : AddCommMonoid N] →
          (f : M →+ N) →
            (∀ (y : ↥S), IsAddUnit (f ↑y)) →
              (∀ (z : N), ∃ x, z + f ↑x.2 = f x.1) →
                (∀ (x y : M), f x = f y → ∃ c, ↑c + x = ↑c + y) → S.LocalizationMap N

Makes a localization map from an AddCommMonoid hom satisfying the characteristic predicate.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

AddCommMonoidAddCommMonoid