mathlib

f066eb1a - feat(algebra/lie/subalgebra): define lattice structure for Lie subalgebras (#6279)

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` and `mem_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. Co-authored-by: Johan Commelin <johan@commelin.net>