Theorems · Theorem · commutative algebra

RingCon.sSup_def

∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (S : Set (RingCon R)), sSup S = ringConGen (sSup (DFunLike.coe '' S))

The supremum of a set of congruence relations is the same as the smallest congruence relation containing the supremum of the set's image under the map to the underlying binary relation.

Defined in

Mathlib.RingTheory.Congruence.Basic

Cited by

1 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMul