Commit 2025-09-19 18:56 bad30a6a
View on Github →feat(Order/Lattice): conditions for an equivalence relation to be a lattice congruence (#26836) Define a structure asserting that a binary relation is a lattice congruence and provide sufficient and necessary conditions. An application is given in #26983