Theorems · Inductive type · group theory

AddSubmonoid.LocalizationMap

{M : Type u_1} → [inst : AddCommMonoid M] → AddSubmonoid M → (N : Type u_2) → [AddCommMonoid N] → Type (max u_1 u_2)

The type of AddMonoid homomorphisms satisfying the characteristic predicate: if f : M →+ N satisfies this predicate, then N is isomorphic to the localization of M at S.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

119 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 27 definitions · uses no axioms

Assumes

AddCommMonoidAddCommMonoid