Theorems · Definition · group theory

AddLocalization.r

{M : Type u_1} → [inst : AddCommMonoid M] → (S : AddSubmonoid M) → AddCon (M × ↥S)

The congruence relation on M × S, M an AddCommMonoid and S an AddSubmonoid of M, whose quotient is the localization of M at S, defined as the unique congruence relation on M × S such that for any other congruence relation s on M × S where for all y ∈ S, (0, 0) ∼ (y, y) under s, we have that (x₁, y₁) ∼ (x₂, y₂) by r implies (x₁, y₁) ∼ (x₂, y₂) by s.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

14 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

AddCommMonoid