Commit 2022-06-04 15:25 b9492402
View on Github →feat(algebra/{lie/subalgebra,module/submodule/pointwise}): submodules and lie subalgebras form canonically ordered additive monoids under addition (#14529)
We can't actually make these instances because they result in loops for simp.
The le_iff_exists_sup lemma is probably not very useful for much beyond these new instances, but it matches le_iff_exists_add.