Theorems · Theorem · commutative algebra

RingCon.sup_eq_ringConGen

∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (c d : RingCon R), c ⊔ d = ringConGen fun x y => c x y ∨ d x y

The supremum of congruence relations c, d equals the smallest congruence relation containing the binary relation 'x is related to y by c or d'.

Defined in: Mathlib.RingTheory.Congruence.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Add Mul

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · cited by 62,936
RingConstatement and proof · cited by 219
ringConGenstatement · cited by 18
RingCon.sup_defproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.