Commit 2024-01-26 19:09 f1802b11
View on Github →feat: Add lattice lemmas about Sub{group,monoid}.{op,unop}
(#9860)
In fact I only need the closure
lemma, but the others are easy enough.
This changes the opEquiv
s to be order isomorphisms rather than just Equiv
s.