Theorems · Inductive type · group theory

Submonoid.LocalizationMap

{M : Type u_1} → [inst : CommMonoid M] → Submonoid M → (N : Type u_2) → [CommMonoid N] → Type (max u_1 u_2)

The type of monoid 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

147 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoid