Commit 2026-06-12 18:57 da8dd888

View on Github →

feat: add missing api about congruence closures (#40480) This tries to make identical changes to the RingCon and Con files; almost all of the properties of the respective ringConGen and conGen closure operators can be derived from the galois insertion, which allows most proofs to be golfed to a single term. conGen_le is changed from an implication to an Iff, to match Submodule.span_le and Submonoid.closure_le.

Estimated changes

added theorem Con.conGen_iSup
modified theorem Con.conGen_idem
modified theorem Con.conGen_le
added theorem Con.conGen_monotone
added theorem Con.conGen_sSup
added theorem Con.conGen_sup
added theorem Con.le_conGen
modified theorem Con.sSup_def
modified theorem Con.sup_def
modified theorem Con.sup_eq_conGen
added theorem RingCon.le_ringConGen
modified theorem RingCon.ringConGen_le
added theorem RingCon.ringConGen_sup
modified theorem RingCon.sSup_def
modified theorem RingCon.sup_def
modified theorem RingCon.sup_eq_ringConGen