Theorems · Theorem · group theory

AddCon.addConGen_eq

∀ {M : Type u_1} [inst : Add M] (r : M → M → Prop), addConGen r = sInf {s | ∀ (x y : M), r x y → s x y}

The inductively defined smallest additive congruence relation containing a binary relation r equals the infimum of the set of additive congruence relations containing r.

Defined in

Mathlib.GroupTheory.Congruence.Defs

Cited by

1 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Quot.sound

Assumes

Add