Commit 2023-12-16 00:58 eb4573aa

View on Github →

feat(RingTheory/Congruence): add the CompleteLattice instance (#8313) The code is copied from GroupTheory/Congruence.lean, and then modified to fix the errors. I haven't copied the full contents of GroupTheory/Congruencee, only the results about the lattice structure. This replaces leanprover-community/mathlib#18588

Estimated changes

added theorem Con.coe_iInf
added theorem RingCon.coe_iInf
added theorem RingCon.coe_inf
added theorem RingCon.coe_sInf
added theorem RingCon.coe_top
added theorem RingCon.ext'
added theorem RingCon.ext
added theorem RingCon.inf_iff_and
added theorem RingCon.le_def
modified theorem RingCon.rel_mk
added theorem RingCon.ringConGen_eq
added theorem RingCon.ringConGen_le
added theorem RingCon.sInf_toSetoid
added theorem RingCon.sSup_def
added theorem RingCon.sup_def