feat(order/modular_lattice): define modular lattices (#5564)
Defines modular lattices
Defines the diamond isomorphisms in a modular lattice
Places `is_modular_lattice` instances on a `distrib_lattice`, the lattice of `subgroup`s of a `comm_group`, and the lattice of `submodule`s of a `module`.
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
