Theorem RingCon.ringConGen_of_ringCon

Modification history

2023-12-16 00:58

Mathlib/RingTheory/Congruence.lean

feat(RingTheory/Congruence): add the `CompleteLattice` instance (#8313) …

Added RingCon.ringConGen_of_ringCon View on Github →