Theorems · Inductive type · group theory

AddSubmonoid.IsLocalizationMap

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

A predicate characterizing homomorphisms between additive monoids M and N that form a commutative triangle with the canonical map from M to its localization at S and some isomorphism between N and the localization.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

18 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

AddCommMonoidAddCommMonoid