Mathlib Map

Theorems · Definition · commutative algebra

ringConGen

{R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → (R → R → Prop) → RingCon R

The inductively defined smallest ring congruence relation containing a given binary relation.

Defined in
Mathlib.RingTheory.Congruence.Defs
Cited by
18 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
AddMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

DividedPowerAlgebra.ringCon · cited by 49DividedPowerAlgebra.ringC…TensorAlgebra.symRingCon · cited by 27TensorAlgebra.symRingConRingCon.gi · cited by 10RingCon.giTwoSidedIdeal.span · cited by 9TwoSidedIdeal.spanRingCon.le_ringConGen · cited by 9RingCon.le_ringConGenLinearAlgebra.FreeProduct.ringCon · cited by 8FreeProduct.ringConRingCon.mapGen · cited by 2RingCon.mapGenRingCon.ringConGen_eq · cited by 2RingCon.ringConGen_eqTensorAlgebra.ringCon · cited by 2TensorAlgebra.ringConRingCon.ringConGen_le · cited by 1RingCon.ringConGen_leRingCon.ringConGen_mono · cited by 1RingCon.ringConGen_monoRingCon.ringConGen_monotone · cited by 1RingCon.ringConGen_monoto…RingCon.sSup_def · cited by 1RingCon.sSup_defRingCon.sup_def · cited by 1RingCon.sup_defRingCon.le_comap_ringConGen · cited by 1RingCon.le_comap_ringConG…RingCon · cited by 219RingConRingConGen.Rel · cited by 5RingConGen.RelringConGenCITED BYCITES

Cites2

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

Cited by28

Results whose statement or proof uses this declaration.