Commit 2021-02-17 11:38 f066eb1a
View on Github →feat(algebra/lie/subalgebra): define lattice structure for Lie subalgebras (#6279) We already have the lattice structure for Lie submodules but not for subalgebras. This is mostly a lightly-edited copy-paste of the corresponding subset of results for Lie submodules that remain true for subalgebras. The results which hold for Lie submodules but not for Lie subalgebras are:
sup_coe_to_submodule
andmem_sup
is_modular_lattice
I have also made a few tweaks to bring the structure and naming of Lie subalgebras a little closer to that of Lie submodules.